`BookProof.ChapterE2.exists_angles_realize` (n : ℕ) (p : Fin n → ℝ) (hp : ∀ i, 0 ≤ p i) (hsum : ∑ i, p i = 1) : ∃ θ : ℕ → ℝ, ∀ i : Fin n, bornProb θ n i = p i

Initializing...

`BookProof.ChapterE2.exists_angles_realize` (n : ℕ) (p : Fin n → ℝ) (hp : ∀ i, 0 ≤ p i) (hsum : ∑ i, p i = 1) : ∃ θ : ℕ → ℝ, ∀ i : Fin n, bornProb θ n i = p i · Prove2Me