Variance.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The weighted Poisson argument and the scalar weight used to balance the Weyl moments. The Bochner and Poisson identities imply the exact bound for the test function, including zero norm values.

def OAI.PositiveEinsteinFour.Variance.derivativeRatio line 21
Source documentation
The derivative of H relative to the derivative of the square root.
```
def derivativeRatio (b : ℝ) : ℝ := 1 + b ^ 2 / 8 - b ^ 4 / 128
```
theorem OAI.PositiveEinsteinFour.Variance.hasDerivAt_H line 23
theorem OAI.PositiveEinsteinFour.Variance.derivativeRatio_bounds line 42
Source documentation
The exact quartic remainder makes the squared derivative ratio small.
```
theorem derivativeRatio_bounds {b : ℝ} (hb : 0 ≤ b) (hb2 : b ≤ 2) :
    0 ≤ derivativeRatio b ∧ (derivativeRatio b) ^ 2 ≤ 1 + b ^ 2 / 4 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Variance.derivativeRatio
theorem OAI.PositiveEinsteinFour.Variance.weighted_H_energy_le line 65
Source documentation
This formulation is defined even at b = 0: the supplied energy is the squared gradient of sqrt b, whose almost-everywhere zero-set convention comes from the geometric regularization argument.
```
theorem weighted_H_energy_le {v b e : ℝ}
    (hb : 0 ≤ b) (hb2 : b ≤ 2) (he : 0 ≤ e) :
    (derivativeRatio b) ^ 2 * e / (4 + v ^ 2 + b ^ 2) ≤ e / 4 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Variance.derivativeRatio

theorem OAI.PositiveEinsteinFour.Variance.integral_pairing_sq_le line 77

Source documentation

An integral version of the closed two-by-two determinant criterion. It needs no square-root integrability assumptions.

theorem integral_pairing_sq_le {Ω : Type*} [MeasurableSpace Ω]
    {μ : Measure Ω} {f g c : Ω → ℝ}
    (hf : Integrable f μ) (hg : Integrable g μ) (hc : Integrable c μ)
    (hf0 : ∀ᵐ ω ∂μ, 0 ≤ f ω) (hg0 : ∀ᵐ ω ∂μ, 0 ≤ g ω)
    (hpoint : ∀ᵐ ω ∂μ, c ω ^ 2 ≤ f ω * g ω) :
    (∫ ω, c ω ∂μ) ^ 2 ≤ (∫ ω, f ω ∂μ) * ∫ ω, g ω ∂μ := by
…

theorem OAI.PositiveEinsteinFour.Variance.variance_le_of_poisson_pairing line 101

Source documentation

Abstract form of the weighted Poisson proof. For the geometric application, f = |grad a|²/K, g = K |grad phi|², and c = -<grad a,grad phi>; integration by parts gives E c = Var a, while the improved Bochner identity gives E g ≤ Var a. Neither geometric identity is assumed to be published.

theorem variance_le_of_poisson_pairing {Ω : Type*} [MeasurableSpace Ω]
    {μ : Measure Ω} {f g c : Ω → ℝ} {V : ℝ}
    (hf : Integrable f μ) (hg : Integrable g μ) (hc : Integrable c μ)
    (hf0 : ∀ᵐ ω ∂μ, 0 ≤ f ω) (hg0 : ∀ᵐ ω ∂μ, 0 ≤ g ω)
    (hpoint : ∀ᵐ ω ∂μ, c ω ^ 2 ≤ f ω * g ω)
    (hV : 0 ≤ V) (hpair : (∫ ω, c ω ∂μ) = V)
    (hbochner : (∫ ω, g ω ∂μ) ≤ V) :
    V ≤ ∫ ω, f ω ∂μ := by
…

theorem OAI.PositiveEinsteinFour.Variance.weighted_inner_sq_le line 119

Source documentation

Pointwise Cauchy--Schwarz with the reciprocal Poisson weight.

theorem weighted_inner_sq_le {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] (a p : E) {K : ℝ} (hK : 0 < K) :
    (-inner ℝ a p) ^ 2 ≤ (‖a‖ ^ 2 / K) * (K * ‖p‖ ^ 2) := by
…

theorem OAI.PositiveEinsteinFour.Variance.bochner_weighted_energy line 135

Source documentation

The scalar consequence of the integrated Bochner identity and the curvature contraction on trace-free Hessians. Here p and s are squared gradient and trace-free Hessian norms, and c is the curvature contraction. The two geometric identities are retained separately, rather than assuming the improved weighted bound as a single premise.

theorem bochner_weighted_energy {Ω : Type*} [MeasurableSpace Ω]
    {μ : Measure Ω} {v b p s c : Ω → ℝ} {L : ℝ}
    (hp : Integrable p μ) (hs : Integrable s μ) (hc : Integrable c μ)
    (hvp : Integrable (fun ω => (v ω ^ 2 + b ω ^ 2) * p ω) μ)
    (hbochner : L = 4 * (∫ ω, p ω ∂μ) + (4 / 3) * ∫ ω, s ω ∂μ)
    (hcurvature : (∫ ω, c ω ∂μ) = 3 * ∫ ω, (v ω ^ 2 + b ω ^ 2) * p ω ∂μ)
    (hoperator : ∀ᵐ ω ∂μ, c ω ≤ 4 * s ω) :
    (∫ ω, (4 + v ω ^ 2 + b ω ^ 2) * p ω ∂μ) ≤ L := by
…

theorem OAI.PositiveEinsteinFour.Variance.H_variance_le line 157

Source documentation

The weight used in the two-moment obstruction satisfies exactly the variance bound needed by balanced_moments. The hypotheses here separate the geometric weighted-variance theorem from the integrated norm equation.

theorem H_variance_le {Ω : Type*} [MeasurableSpace Ω]
    {μ : Measure Ω} {v b e : Ω → ℝ}
    (he : Integrable e μ)
    (hweighted : Integrable (fun ω => (derivativeRatio (b ω)) ^ 2 * e ω /
      (4 + v ω ^ 2 + b ω ^ 2)) μ)
    (hb : ∀ᵐ ω ∂μ, b ω ∈ Set.Icc (0 : ℝ) 2)
    (he0 : ∀ᵐ ω ∂μ, 0 ≤ e ω)
    (hvariance : (∫ ω, MomentObstruction.H (b ω) ^ 2 ∂μ) -
      (∫ ω, MomentObstruction.H (b ω) ∂μ) ^ 2 ≤
      ∫ ω, (derivativeRatio (b ω)) ^ 2 * e ω / (4 + v ω ^ 2 + b ω ^ 2) ∂μ)
    (hnorm : (4 / 9) * (∫ ω, e ω ∂μ) ≤
      (∫ ω, b ω ^ 2 ∂μ) - ∫ ω, b ω ∂μ) :
…

Mentions: OAI.PositiveEinsteinFour.Variance.derivativeRatio, OAI.PositiveEinsteinFour.MomentObstruction.H