MomentObstruction.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

A direct polynomial proof of the manuscript's two-constrained-moments obstruction. The variable x is sqrt(z/2). Four rational interval certificates replace the compact-measure optimization argument.

def OAI.PositiveEinsteinFour.MomentObstruction.rootWeight line 18
def OAI.PositiveEinsteinFour.MomentObstruction.rootMoment line 19
def OAI.PositiveEinsteinFour.MomentObstruction.constraint line 20
def OAI.PositiveEinsteinFour.MomentObstruction.potential line 21
def OAI.PositiveEinsteinFour.MomentObstruction.lowerPolynomial line 22
def OAI.PositiveEinsteinFour.MomentObstruction.dualPolynomial line 23
theorem OAI.PositiveEinsteinFour.MomentObstruction.lower_cert line 27
theorem OAI.PositiveEinsteinFour.MomentObstruction.dual_cert_0 line 56
theorem OAI.PositiveEinsteinFour.MomentObstruction.dual_cert_1 line 82
theorem OAI.PositiveEinsteinFour.MomentObstruction.dual_cert_2 line 108
theorem OAI.PositiveEinsteinFour.MomentObstruction.dual_cert_3 line 134
theorem OAI.PositiveEinsteinFour.MomentObstruction.potential_lower line 160
theorem OAI.PositiveEinsteinFour.MomentObstruction.dual_lower line 168
theorem OAI.PositiveEinsteinFour.MomentObstruction.rootMoment_nonneg line 178
theorem OAI.PositiveEinsteinFour.MomentObstruction.dual_bound line 187
Source documentation
The pointwise dual inequality, uniform in the scalar mean parameter.
```
theorem dual_bound {x : ℝ} (hx : 0 ≤ x) (hx1 : x ≤ 1) (t : ℝ) :
    1 / 100 ≤ potential x - 64 * t * rootMoment x + 32 * t ^ 2 +
      ((33 / 50) * t - 403 / 2000) * constraint x := by
…
```
Mentions: OAI.PositiveEinsteinFour.MomentObstruction.potential, OAI.PositiveEinsteinFour.MomentObstruction.rootMoment, OAI.PositiveEinsteinFour.MomentObstruction.constraint
theorem OAI.PositiveEinsteinFour.MomentObstruction.integrable_comp_interval line 200
theorem OAI.PositiveEinsteinFour.MomentObstruction.normalized_moment_obstruction line 211
Source documentation
The two-moment obstruction in the coordinate x = sqrt(z/2). The proof uses the explicit dual polynomial; no compactness or extremal-support input is assumed.
```
theorem normalized_moment_obstruction {Ω : Type*} [MeasurableSpace Ω]
    {μ : Measure Ω} [IsProbabilityMeasure μ] {x : Ω → ℝ}
    (hxm : AEStronglyMeasurable x μ) (hx : ∀ᵐ ω ∂μ, x ω ∈ Set.Icc (0 : ℝ) 1)
    (hgap : 1 ≤ ∫ ω, 4 * x ω ^ 4 ∂μ)
    (hconstraint : (∫ ω, constraint (x ω) ∂μ) ≤ 0) :
    32 * (∫ ω, rootMoment (x ω) ∂μ) ^ 2 - ∫ ω, potential (x ω) ∂μ < 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.MomentObstruction.constraint, OAI.PositiveEinsteinFour.MomentObstruction.rootMoment, OAI.PositiveEinsteinFour.MomentObstruction.potential
def OAI.PositiveEinsteinFour.MomentObstruction.H line 265
Source documentation
The scalar test function in the manuscript.
```
def H (z : ℝ) : ℝ := Real.sqrt z * (1 + z ^ 2 / 40 - z ^ 4 / 1152)
```
def OAI.PositiveEinsteinFour.MomentObstruction.Phi line 267
theorem OAI.PositiveEinsteinFour.MomentObstruction.H_two_mul_sq line 269
theorem OAI.PositiveEinsteinFour.MomentObstruction.Phi_two_mul_sq line 275

theorem OAI.PositiveEinsteinFour.MomentObstruction.two_constrained_moments line 284

Source documentation

The original two-constrained-moments lemma, with no regularity beyond measurability of the bounded scalar variable.

theorem two_constrained_moments {Ω : Type*} [MeasurableSpace Ω]
    {μ : Measure Ω} [IsProbabilityMeasure μ] {z : Ω → ℝ}
    (hzm : AEStronglyMeasurable z μ) (hz : ∀ᵐ ω ∂μ, z ω ∈ Set.Icc (0 : ℝ) 2)
    (hgap : 1 ≤ ∫ ω, z ω ^ 2 ∂μ)
    (hconstraint : (∫ ω, 28 * z ω + 6 * z ω ^ 2 ∂μ) ≤ 25) :
    16 * (∫ ω, H (z ω) ∂μ) ^ 2 - ∫ ω, Phi (z ω) ∂μ < 0 := by
…

Mentions: OAI.PositiveEinsteinFour.MomentObstruction.H, OAI.PositiveEinsteinFour.MomentObstruction.Phi