OAI/Geometry/EinsteinFour/NormVarianceApproximation.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Dominated smooth approximation of both Weyl norms and their difference. The gradient limit uses the actual zero-set support property.

  1. theorem OAI.PositiveEinsteinFour.Variance.contDiff_hRegularizedArgument line 15
  2. theorem OAI.PositiveEinsteinFour.Variance.contDiff_hRegularizedValue line 20
  3. def OAI.PositiveEinsteinFour.Variance.regularizedRadialVector line 29
  4. def OAI.PositiveEinsteinFour.Variance.regularizedNormEnergy line 32
  5. def OAI.PositiveEinsteinFour.Variance.regularizedDifferenceValue line 35
  6. def OAI.PositiveEinsteinFour.Variance.regularizedDifferenceEnergy line 38
  7. theorem OAI.PositiveEinsteinFour.Variance.regularizedRadialVector_norm_le line 41
  8. theorem OAI.PositiveEinsteinFour.Variance.regularizedDifference_square_le line 50
  9. theorem OAI.PositiveEinsteinFour.Variance.regularizedDifferenceEnergy_nonneg line 61
  10. theorem OAI.PositiveEinsteinFour.Variance.regularizedDifferenceEnergy_le line 64
  11. theorem OAI.PositiveEinsteinFour.Variance.normDifferenceEnergy_le line 75
  12. theorem OAI.PositiveEinsteinFour.Variance.tendsto_regularizedRadialVector line 86
  13. theorem OAI.PositiveEinsteinFour.Variance.tendsto_regularizedDifferenceValue line 99
  14. theorem OAI.PositiveEinsteinFour.Variance.tendsto_regularizedDifferenceEnergy line 103
  15. theorem OAI.PositiveEinsteinFour.Variance.regularizedNormEnergy_eq_difference line 110
  16. theorem OAI.PositiveEinsteinFour.Variance.regularizedDifferenceValue_abs_le line 114
  17. theorem OAI.PositiveEinsteinFour.Variance.aestronglyMeasurable_regularizedRadialVector line 127
  18. theorem OAI.PositiveEinsteinFour.Variance.integrable_normDifferenceEnergy line 133
  19. theorem OAI.PositiveEinsteinFour.Variance.integral_regularizedDifferenceEnergy_tendsto line 145
  20. theorem OAI.PositiveEinsteinFour.Variance.integral_regularizedNormEnergy_tendsto line 169
  21. theorem OAI.PositiveEinsteinFour.Variance.integral_regularizedNorm_pow_tendsto line 184
  22. theorem OAI.PositiveEinsteinFour.Variance.integral_regularizedDifferenceValue_pow_tendsto line 202
  23. theorem OAI.PositiveEinsteinFour.Variance.variance_congr_ae line 224

    Source documentation

    Difference-of-moments variance depends only on the almost-everywhere class.

    theorem variance_congr_ae {f g : Ω → ℝ} (hfg : f =ᵐ[μ] g) :
    (∫ x, f x ^ 2 ∂μ) - (∫ x, f x ∂μ) ^ 2 =
      (∫ x, g x ^ 2 ∂μ) - (∫ x, g x ∂μ) ^ 2 := by
…
  24. theorem OAI.PositiveEinsteinFour.Variance.integral_centered_square line 233

    Source documentation

    For probability measure, the centered-square and difference-of-moments forms agree under precisely the first and second moment integrability.

    theorem integral_centered_square [IsProbabilityMeasure μ] {f : Ω → ℝ}
    (hf : Integrable f μ) (hf2 : Integrable (fun x => f x ^ 2) μ) :
    (∫ x, (f x - ∫ y, f y ∂μ) ^ 2 ∂μ) =
      (∫ x, f x ^ 2 ∂μ) - (∫ x, f x ∂μ) ^ 2 := by
…
  25. theorem OAI.PositiveEinsteinFour.Variance.difference_variance_of_regularized line 249

    Source documentation

    The weighted variance for the difference of actual norms follows by smooth approximation and the separately proved zero-set support.

    theorem difference_variance_of_regularized [IsFiniteMeasure μ] {v b K : Ω → ℝ} {p q : Ω → F}
    (hv : AEMeasurable v μ) (hb : AEMeasurable b μ) (hK : AEMeasurable K μ)
    (hp : AEStronglyMeasurable p μ) (hq : AEStronglyMeasurable q μ)
    (hv2 : ∀ᵐ x ∂μ, v x ∈ Set.Icc (0 : ℝ) 2)
    (hb2 : ∀ᵐ x ∂μ, b x ∈ Set.Icc (0 : ℝ) 2)
    (hK1 : ∀ᵐ x ∂μ, 1 ≤ K x)
    (hp0 : ∀ᵐ x ∂μ, v x = 0 → p x = 0) (hq0 : ∀ᵐ x ∂μ, b x = 0 → q x = 0)
    (hp2 : Integrable (fun x => ‖p x‖ ^ 2) μ) (hq2 : Integrable (fun x => ‖q x‖ ^ 2) μ)
    (ε : ℕ → ℝ) (hε : ∀ n, ε n ∈ Set.Ioc (0 : ℝ) 1)
    (hlim : Tendsto ε atTop (𝓝 0))
    (hvariance : ∀ n, (∫ x, regularizedDifferenceValue (v x) (b x) (ε n) ^ 2 ∂μ) -
      (∫ x, regularizedDifferenceValue (v x) (b x) (ε n) ∂μ) ^ 2 ≤
…

    Mentions: OAI.PositiveEinsteinFour.Variance.regularizedDifferenceValue

  26. theorem OAI.PositiveEinsteinFour.Variance.norm_variance_of_regularized line 274

    Source documentation

    Either single norm is obtained by the same approximation, with its own actual radial gradient and zero-set support.

    theorem norm_variance_of_regularized [IsFiniteMeasure μ] {v K : Ω → ℝ} {p : Ω → F}
    (hv : AEMeasurable v μ) (hK : AEMeasurable K μ) (hp : AEStronglyMeasurable p μ)
    (hv2 : ∀ᵐ x ∂μ, v x ∈ Set.Icc (0 : ℝ) 2) (hK1 : ∀ᵐ x ∂μ, 1 ≤ K x)
    (hp0 : ∀ᵐ x ∂μ, v x = 0 → p x = 0) (hp2 : Integrable (fun x => ‖p x‖ ^ 2) μ)
    (ε : ℕ → ℝ) (hε : ∀ n, ε n ∈ Set.Ioc (0 : ℝ) 1)
    (hlim : Tendsto ε atTop (𝓝 0))
    (hvariance : ∀ n, (∫ x, hRegularizedArgument (v x) (ε n) ^ 2 ∂μ) -
      (∫ x, hRegularizedArgument (v x) (ε n) ∂μ) ^ 2 ≤
        ∫ x, regularizedNormEnergy (v x) (ε n) (K x) (p x) ∂μ) :
    (∫ x, v x ^ 2 ∂μ) - (∫ x, v x ∂μ) ^ 2 ≤ ∫ x, ‖p x‖ ^ 2 / K x ∂μ := by
…

    Mentions: OAI.PositiveEinsteinFour.Variance.hRegularizedArgument, OAI.PositiveEinsteinFour.Variance.regularizedNormEnergy