`BookProof.ChapterU.portfolio_std_inv_sqrt` {n : ℕ} (hn : 0 < n) (X : Fin n → Ω → ℝ) (σ : ℝ) (hσ : 0 ≤ σ) (P : Measure Ω) [IsProbabilityMeasure P] (hindep : ProbabilityTheory.iInde

Proved

BookProof.ChapterU.portfolio_std_inv_sqrt

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterU.

BookProof.ChapterU.portfolio_std_inv_sqrt {n : ℕ} (hn : 0 < n) (X : Fin n → Ω → ℝ) (σ : ℝ) (hσ : 0 ≤ σ) (P : Measure Ω) [IsProbabilityMeasure P] (hindep : ProbabilityTheory.iIndepFun X P) (hmem : ∀ i, MemLp (X i) 2 P) (hvar : ∀ i, ProbabilityTheory.variance (X i) P = σ ^ 2) : Real.sqrt (ProbabilityTheory.variance (fun ω => (∑ i, X i ω) / n) P) = σ / Real.sqrt n

Formalization note: Lean 4 identifier BookProof.ChapterU.portfolio_std_inv_sqrt.

Preamble

-- Generated from ChapterU.lean — theorem BookProof.ChapterU.portfolio_std_inv_sqrt
import Mathlib
import Definitions.Def_ChapterU
open BookProof.ChapterU


open MeasureTheory
open scoped ENNReal ProbabilityTheory TensorProduct

variable {X : Type*} [MeasurableSpace X]
variable (R M N : Type*) [CommRing R] [AddCommGroup M] [Module R M]
  [AddCommGroup N] [Module R N]
variable {Ω : Type*} [MeasurableSpace Ω]

Formal statement

theorem BookProof.ChapterU.portfolio_std_inv_sqrt {n : ℕ} (hn : 0 < n) (X : Fin n → Ω → ℝ) (σ : ℝ)
    (hσ : 0 ≤ σ) (P : Measure Ω) [IsProbabilityMeasure P]
    (hindep : ProbabilityTheory.iIndepFun X P)
    (hmem : ∀ i, MemLp (X i) 2 P) (hvar : ∀ i, ProbabilityTheory.variance (X i) P = σ ^ 2) :
    Real.sqrt (ProbabilityTheory.variance (fun ω => (∑ i, X i ω) / n) P) = σ / Real.sqrt n := by sorry

View graph