OAI/Geometry/EinsteinFour/HVarianceApproximation.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Smooth approximation of the scalar test used in the weighted-variance argument, with domination by the actual square-root energy.

  1. def OAI.PositiveEinsteinFour.Variance.hRegularizedArgument line 16
  2. def OAI.PositiveEinsteinFour.Variance.hRegularizedValue line 18
  3. def OAI.PositiveEinsteinFour.Variance.hRegularizedDerivative line 20
  4. def OAI.PositiveEinsteinFour.Variance.hRegularizedEnergy line 24
  5. def OAI.PositiveEinsteinFour.Variance.hLimitEnergy line 28
  6. theorem OAI.PositiveEinsteinFour.Variance.hRegularizedArgument_pos line 30
  7. theorem OAI.PositiveEinsteinFour.Variance.le_hRegularizedArgument line 36
  8. theorem OAI.PositiveEinsteinFour.Variance.hRegularizedArgument_le_three line 42
  9. theorem OAI.PositiveEinsteinFour.Variance.continuous_hRegularizedArgument line 54
  10. theorem OAI.PositiveEinsteinFour.Variance.continuous_H line 59
  11. theorem OAI.PositiveEinsteinFour.Variance.hRegularizedArgument_zero line 63
  12. theorem OAI.PositiveEinsteinFour.Variance.hasDerivAt_hRegularizedArgument line 68
  13. theorem OAI.PositiveEinsteinFour.Variance.hasDerivAt_hRegularizedValue line 78
  14. theorem OAI.PositiveEinsteinFour.Variance.hRegularizedDerivative_sq line 83
  15. theorem OAI.PositiveEinsteinFour.Variance.hRegularizedEnergy_eq_derivative line 94
  16. theorem OAI.PositiveEinsteinFour.Variance.hRegularizedGradient_energy line 100
  17. theorem OAI.PositiveEinsteinFour.Variance.hLimitEnergy_sqrt_energy line 106
  18. theorem OAI.PositiveEinsteinFour.Variance.derivativeRatio_bounds_three line 111
  19. theorem OAI.PositiveEinsteinFour.Variance.hRegularizedEnergy_nonneg line 123
  20. theorem OAI.PositiveEinsteinFour.Variance.hRegularizedEnergy_le line 130

    Source documentation

    Uniform domination includes the zero face with Lean's totalized division.

    theorem hRegularizedEnergy_le {b ε E K : ℝ} (hb : b ∈ Set.Icc (0 : ℝ) 2)
    (hε : ε ∈ Set.Ioc (0 : ℝ) 1) (hE : 0 ≤ E) (hK : 1 ≤ K) :
    hRegularizedEnergy b ε E K ≤ E / b := by
…

    Mentions: OAI.PositiveEinsteinFour.Variance.hRegularizedEnergy

  21. theorem OAI.PositiveEinsteinFour.Variance.tendsto_hRegularizedArgument line 160
  22. theorem OAI.PositiveEinsteinFour.Variance.tendsto_hRegularizedValue line 166
  23. theorem OAI.PositiveEinsteinFour.Variance.tendsto_hRegularizedEnergy line 170
  24. theorem OAI.PositiveEinsteinFour.Variance.abs_H_le_four line 189
  25. theorem OAI.PositiveEinsteinFour.Variance.hLimitEnergy_nonneg line 206
  26. theorem OAI.PositiveEinsteinFour.Variance.hLimitEnergy_le line 211
  27. theorem OAI.PositiveEinsteinFour.Variance.aemeasurable_hRegularizedArgument line 228
  28. theorem OAI.PositiveEinsteinFour.Variance.aemeasurable_hRegularizedValue line 232
  29. theorem OAI.PositiveEinsteinFour.Variance.aemeasurable_hRegularizedEnergy line 236
  30. theorem OAI.PositiveEinsteinFour.Variance.integrable_hLimitEnergy line 245
  31. theorem OAI.PositiveEinsteinFour.Variance.integral_hRegularizedEnergy_tendsto line 260
  32. theorem OAI.PositiveEinsteinFour.Variance.integral_hRegularizedValue_pow_tendsto line 281
  33. theorem OAI.PositiveEinsteinFour.Variance.H_variance_of_regularized line 302

    Source documentation

    Smooth weighted variance passes to the singular square-root test with an actual integrable domination, rather than a formal limiting premise.

    theorem H_variance_of_regularized [IsFiniteMeasure μ] {b E K : Ω → ℝ}
    (hb : AEMeasurable b μ) (hE : AEMeasurable E μ) (hK : AEMeasurable K μ)
    (hb2 : ∀ᵐ x ∂μ, b x ∈ Set.Icc (0 : ℝ) 2)
    (hE0 : ∀ᵐ x ∂μ, 0 ≤ E x) (hK1 : ∀ᵐ x ∂μ, 1 ≤ K x)
    (hdom : Integrable (fun x => E x / b x) μ)
    (ε : ℕ → ℝ) (hε : ∀ n, ε n ∈ Set.Ioc (0 : ℝ) 1)
    (hlim : Tendsto ε atTop (𝓝 0))
    (hvariance : ∀ n, (∫ x, hRegularizedValue (b x) (ε n) ^ 2 ∂μ) -
      (∫ x, hRegularizedValue (b x) (ε n) ∂μ) ^ 2 ≤
        ∫ x, hRegularizedEnergy (b x) (ε n) (E x) (K x) ∂μ) :
    (∫ x, MomentObstruction.H (b x) ^ 2 ∂μ) -
      (∫ x, MomentObstruction.H (b x) ∂μ) ^ 2 ≤
…

    Mentions: OAI.PositiveEinsteinFour.Variance.hRegularizedValue, OAI.PositiveEinsteinFour.Variance.hRegularizedEnergy, OAI.PositiveEinsteinFour.MomentObstruction.H