OAI/Geometry/ProjectionBodies/NormEstimates.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PettyProjection.Spherical.mean_add line 12
2. lemma OAI.PettyProjection.Spherical.mean_sub line 16
3. lemma OAI.PettyProjection.Spherical.mean_const_mul line 20
4. lemma OAI.PettyProjection.Spherical.mean_mul_const line 23
5. lemma OAI.PettyProjection.Spherical.mean_div_const line 26
6. lemma OAI.PettyProjection.Spherical.mean_mono line 29
7. lemma OAI.PettyProjection.Spherical.mean_nonneg line 33
8. lemma OAI.PettyProjection.Spherical.mean_centered_square line 36
9. lemma OAI.PettyProjection.Spherical.norm_Q_le_variance line 49
10. lemma OAI.PettyProjection.Spherical.weighted_square_bound line 53
11. lemma OAI.PettyProjection.Spherical.weighted_norm_bound line 62
12. lemma OAI.PettyProjection.Spherical.scalar_correction line 68
13. lemma OAI.PettyProjection.Spherical.scalar_curvature line 93
14. lemma OAI.PettyProjection.Spherical.continuous_e_comp line 111
15. lemma OAI.PettyProjection.Spherical.continuous_M_comp line 115
16. lemma OAI.PettyProjection.Spherical.mean_e_zero line 120
17. lemma OAI.PettyProjection.Spherical.mean_M_of_normalized line 126
18. lemma OAI.PettyProjection.Spherical.mean_W_of_normalized line 136
19. lemma OAI.PettyProjection.Spherical.mean_first_power_ge_one line 146
20. lemma OAI.PettyProjection.Spherical.norm_mean_ranges line 154
21. lemma OAI.PettyProjection.Spherical.continuous_D line 194
22. lemma OAI.PettyProjection.Spherical.continuous_L line 197
23. lemma OAI.PettyProjection.Spherical.continuous_W_comp line 202
24. lemma OAI.PettyProjection.Spherical.mean_D line 206
25. lemma OAI.PettyProjection.Spherical.mean_L line 215
26. lemma OAI.PettyProjection.Spherical.Q_power_split line 240
27. lemma OAI.PettyProjection.Spherical.norm_reduction line 252

    Source documentation

    Exact expectation reduction in the proof of the norm theorem.

    lemma norm_reduction {n : ℕ} (hn : 4 ≤ n) [NeZero n] (g : Seminorm ℝ (Space n)) :
        coefficient n * ‖Q n (toH n (restrictContinuous (fun x => g x ^ exponent n)
          ((seminorm_continuous n g).pow _)))‖^2 ≤
          mean (fun u : Sphere n => L n (g u)) + coefficient n *
            (2*n*(mean (fun u : Sphere n => G n (g u)))^2/(weight n*(2*n+8)) -
              (mean (fun u : Sphere n => D n (g u)))^2/(1-weight n)) := by
    …

    Mentions: OAI.PettyProjection.Spherical.Space, OAI.PettyProjection.Spherical.Q, OAI.PettyProjection.Spherical.toH, OAI.PettyProjection.Spherical.restrictContinuous, OAI.PettyProjection.Spherical.seminorm_continuous, OAI.PettyProjection.Spherical.mean, OAI.PettyProjection.Spherical.Sphere

28. lemma OAI.PettyProjection.Spherical.mean_square_remainder line 290
29. lemma OAI.PettyProjection.Spherical.scalar_expectation line 307
30. theorem OAI.PettyProjection.Spherical.norm_estimate line 333

    Source documentation

    The full arbitrary-norm estimate, including strictness. It uses the actual spherical measure and the actual quadratic-removing Q.

    theorem norm_estimate {n : ℕ} (hn : 4 ≤ n) [NeZero n]
        (g : Seminorm ℝ (Space n)) (hg : ∀ u : Sphere n, 0 < g u)
        (hnorm : mean (fun u : Sphere n => (g u)⁻¹^n) = 1) :
        coefficient n * ‖Q n (toH n (restrictContinuous (fun x => g x ^ exponent n)
          ((seminorm_continuous n g).pow _)))‖^2 ≤
          (mean (fun u : Sphere n => (g u)^exponent n))^2 -
            (mean (fun u : Sphere n => (g u)^(exponent n-1)))^2 ∧
        (coefficient n * ‖Q n (toH n (restrictContinuous (fun x => g x ^ exponent n)
          ((seminorm_continuous n g).pow _)))‖^2 =
          (mean (fun u : Sphere n => (g u)^exponent n))^2 -
            (mean (fun u : Sphere n => (g u)^(exponent n-1)))^2 ↔ ∀ u : Sphere n, g u = 1) := by
    …

    Mentions: OAI.PettyProjection.Spherical.Space, OAI.PettyProjection.Spherical.Sphere, OAI.PettyProjection.Spherical.mean, OAI.PettyProjection.Spherical.Q, OAI.PettyProjection.Spherical.toH, OAI.PettyProjection.Spherical.restrictContinuous, OAI.PettyProjection.Spherical.seminorm_continuous