Balanced.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The scalar assembly of the balanced-Weyl-moments argument. The upper volume estimate and the weighted variance estimate remain separate geometric obligations; neither is declared to be a published input here.

theorem OAI.PositiveEinsteinFour.J_nonneg_of_variance line 16

theorem OAI.PositiveEinsteinFour.ordered_balanced_moments line 37

Source documentation

In the ordered case, the exact integer and moment constraints force equal moments once the two-constrained-moments obstruction is applied.

theorem ordered_balanced_moments {Ω : Type*} [MeasurableSpace Ω]
    {μ : Measure Ω} [IsProbabilityMeasure μ] {v b : Ω → ℝ}
    (n m : ℕ) (volume : ℝ)
    (hbm : AEStronglyMeasurable b μ)
    (hv : ∀ᵐ ω ∂μ, v ω ∈ Set.Icc (0 : ℝ) 2)
    (hb : ∀ᵐ ω ∂μ, b ω ∈ Set.Icc (0 : ℝ) 2)
    (hsum : ∀ᵐ ω ∂μ, v ω + b ω ≤ 2)
    (hbi : Integrable b μ)
    (hv2i : Integrable (fun ω => v ω ^ 2) μ)
    (hb2i : Integrable (fun ω => b ω ^ 2) μ)
    (hHbi : Integrable (fun ω => H (b ω) ^ 2) μ)
    (hvgap : 1 ≤ ∫ ω, v ω ^ 2 ∂μ) (hbgap : 1 ≤ ∫ ω, b ω ^ 2 ∂μ)
…

theorem OAI.PositiveEinsteinFour.balanced_moments line 97

Source documentation

Symmetric scalar form of the balanced-moment conclusion. The geometric volume and weighted-variance estimates are explicit premises, pending their independent formalization.

theorem balanced_moments {Ω : Type*} [MeasurableSpace Ω]
    {μ : Measure Ω} [IsProbabilityMeasure μ] {v b : Ω → ℝ}
    (n m : ℕ) (volume : ℝ)
    (hvm : AEStronglyMeasurable v μ) (hbm : AEStronglyMeasurable b μ)
    (hv : ∀ᵐ ω ∂μ, v ω ∈ Set.Icc (0 : ℝ) 2)
    (hb : ∀ᵐ ω ∂μ, b ω ∈ Set.Icc (0 : ℝ) 2)
    (hsum : ∀ᵐ ω ∂μ, v ω + b ω ≤ 2)
    (hvi : Integrable v μ) (hbi : Integrable b μ)
    (hv2i : Integrable (fun ω => v ω ^ 2) μ)
    (hb2i : Integrable (fun ω => b ω ^ 2) μ)
    (hHvi : Integrable (fun ω => H (v ω) ^ 2) μ)
    (hHbi : Integrable (fun ω => H (b ω) ^ 2) μ)
…