OAI/Geometry/ProjectionBodies/NormRigidity.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PettyProjection.Spherical.norm_gradient_eq line 10
2. lemma OAI.PettyProjection.Spherical.gradient_pow line 14
3. lemma OAI.PettyProjection.Spherical.signField_eq_gradient line 21
4. lemma OAI.PettyProjection.Spherical.norm_signField_le line 27
5. lemma OAI.PettyProjection.Spherical.normSmooth_powerField_bound line 42
6. lemma OAI.PettyProjection.Spherical.normSmooth_powerField_tendsto line 76
7. lemma OAI.PettyProjection.Spherical.signedPair_tendsto line 97
8. lemma OAI.PettyProjection.Spherical.ae_bound_of_limit line 117
9. lemma OAI.PettyProjection.Spherical.signedPair_integrable_of_ae_bound line 124
10. lemma OAI.PettyProjection.Spherical.inner_Q_Q_expand line 149
11. lemma OAI.PettyProjection.Spherical.sign_spectral_estimate_with_two line 163
12. lemma OAI.PettyProjection.Spherical.sign_form_estimate_with_two line 190
13. lemma OAI.PettyProjection.Spherical.normSmooth_power_restrict_tendsto line 212
14. lemma OAI.PettyProjection.Spherical.norm_signedPair_tendsto line 221
15. theorem OAI.PettyProjection.Spherical.norm_sign_form line 236

    Source documentation

    The sign-transform lower bound for powers of arbitrary nonsmooth norms.

    theorem norm_sign_form {n : ℕ} (hn : 2 ≤ n) [NeZero n]
        (f g : Seminorm ℝ (Space n)) {k : ℕ} (hk : 0 < k)
        (h2 : (harmonicSpace n 2).starProjection (toH n
          (restrictContinuous (fun x => f x^k) ((seminorm_continuous n f).pow k))) = 0) :
        mean (fun u : Sphere n => f u^k)*mean (fun u : Sphere n => g u^k) -
          ((1+(2/(k : ℝ)+((n : ℝ)-1)/(k : ℝ)^2)*(4*(n+2)))/((n+1)*(n+3)))*
            ‖Q n (toH n (restrictContinuous (fun x => f x^k) ((seminorm_continuous n f).pow k)))‖*
            ‖Q n (toH n (restrictContinuous (fun x => g x^k) ((seminorm_continuous n g).pow k)))‖ ≤
          signedPair (signField (k : ℝ) (fun x => f x^k))
            (signField (k : ℝ) (fun x => g x^k))/cosineConstant n := by
    …

    Mentions: OAI.PettyProjection.Spherical.Space, OAI.PettyProjection.Spherical.harmonicSpace, OAI.PettyProjection.Spherical.toH, OAI.PettyProjection.Spherical.restrictContinuous, OAI.PettyProjection.Spherical.seminorm_continuous, OAI.PettyProjection.Spherical.mean, OAI.PettyProjection.Spherical.Sphere, OAI.PettyProjection.Spherical.Q, OAI.PettyProjection.Spherical.signedPair, OAI.PettyProjection.Spherical.signField, OAI.PettyProjection.Spherical.cosineConstant

16. lemma OAI.PettyProjection.Spherical.reverse_lorentz line 272
17. lemma OAI.PettyProjection.Spherical.reverse_lorentz_strict line 282
18. lemma OAI.PettyProjection.Spherical.coefficient_sign_factor line 305
19. def OAI.PettyProjection.Spherical.gaugeMoment line 326
20. def OAI.PettyProjection.Spherical.gaugeTail line 329
21. lemma OAI.PettyProjection.Spherical.gaugeMoment_ranges line 332
22. lemma OAI.PettyProjection.Spherical.gaugeTail_of_one line 346
23. lemma OAI.PettyProjection.Spherical.scaled_norm_energy line 353
24. lemma OAI.PettyProjection.Spherical.normalized_one_eq line 398
25. lemma OAI.PettyProjection.Spherical.seminorm_euler line 433
26. def OAI.PettyProjection.Spherical.gaugeField line 446
27. lemma OAI.PettyProjection.Spherical.signField_power_eq line 449
28. lemma OAI.PettyProjection.Spherical.signField_power_ae_eq line 467
29. lemma OAI.PettyProjection.Spherical.gaugeField_measurable_bound line 472
30. lemma OAI.PettyProjection.Spherical.signedPair_congr_ae line 485
31. lemma OAI.PettyProjection.Spherical.signedPair_gaugeField line 494
32. def OAI.PettyProjection.Spherical.absolutePair line 499
33. lemma OAI.PettyProjection.Spherical.gaugeField_absolute_integrable line 502
34. lemma OAI.PettyProjection.Spherical.signedPair_gaugeField_le_absolute line 519
35. lemma OAI.PettyProjection.Spherical.norm_absolutePair_lower line 539
36. theorem OAI.PettyProjection.Spherical.normalized_norm_pair line 554

    Source documentation

    Spherical form of the full bilinear estimate, before construction of the variational representing bodies. Both norms can be nonsmooth.

    theorem normalized_norm_pair {n : ℕ} (hn : 4 ≤ n) [NeZero n]
        (f g : Seminorm ℝ (Space n)) (hf : ∀ u : Sphere n, 0 < f u) (hg : ∀ u : Sphere n, 0 < g u)
        (hfn : mean (fun u : Sphere n => (f u)⁻¹^n) = 1)
        (hgn : mean (fun u : Sphere n => (g u)⁻¹^n) = 1)
        (h2 : (harmonicSpace n 2).starProjection (toH n
          (restrictContinuous (fun x => f x^exponent n) ((seminorm_continuous n f).pow _))) = 0)
        {s t : ℝ} (hs : 0 < s) (ht : 0 < t)
        (hsf : 1 ≤ s*gaugeMoment f (exponent n-1)) (htg : 1 ≤ t*gaugeMoment g (exponent n-1)) :
        cosineConstant n ≤ s*t*absolutePair (gaugeField f (exponent n)) (gaugeField g (exponent n)) ∧
        (s*t*absolutePair (gaugeField f (exponent n)) (gaugeField g (exponent n)) = cosineConstant n →
          (∀ u : Sphere n, f u = 1) ∧ (∀ u : Sphere n, g u = 1) ∧ s = 1 ∧ t = 1) := by
    …

    Mentions: OAI.PettyProjection.Spherical.Space, OAI.PettyProjection.Spherical.Sphere, OAI.PettyProjection.Spherical.mean, OAI.PettyProjection.Spherical.harmonicSpace, OAI.PettyProjection.Spherical.toH, OAI.PettyProjection.Spherical.restrictContinuous, OAI.PettyProjection.Spherical.seminorm_continuous, OAI.PettyProjection.Spherical.gaugeMoment, OAI.PettyProjection.Spherical.cosineConstant, OAI.PettyProjection.Spherical.absolutePair, OAI.PettyProjection.Spherical.gaugeField