OAI/Geometry/ProjectionBodies/NormCurvature.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PettyProjection.wulff line 13

   Source documentation

   Intersection of the actual supporting constraints, with no evenness or convexity condition on the constraint function.

   def wulff {n : ℕ} (s : Sphere n → ℝ) : Set (Space n) :=
   …

   Mentions: OAI.PettyProjection.Space

2. lemma OAI.PettyProjection.wulff_closed line 16
3. lemma OAI.PettyProjection.wulff_convex line 21
4. lemma OAI.PettyProjection.closedBall_subset_wulff line 29
5. lemma OAI.PettyProjection.wulff_subset_closedBall line 38
6. lemma OAI.PettyProjection.positive_constraint_bounds line 53
7. lemma OAI.PettyProjection.wulff_nhds line 62
8. lemma OAI.PettyProjection.wulff_compact line 68
9. lemma OAI.PettyProjection.wulff_body line 74
10. lemma OAI.PettyProjection.wulff_support line 78
11. def OAI.PettyProjection.wulffCoefficients line 98

    Source documentation

    Compact coefficient set of the maximum formula.

    def wulffCoefficients {n : ℕ} (s : Sphere n → ℝ) : Set (Space n) :=
    …

    Mentions: OAI.PettyProjection.Space

12. def OAI.PettyProjection.wulffMax line 101
13. lemma OAI.PettyProjection.wulffCoefficients_compact line 104
14. lemma OAI.PettyProjection.wulffCoefficients_nonempty line 108
15. lemma OAI.PettyProjection.wulffMax_attained line 113
16. lemma OAI.PettyProjection.le_wulffMax line 119
17. lemma OAI.PettyProjection.wulffMax_pos line 124
18. lemma OAI.PettyProjection.wulffMax_zero line 137
19. lemma OAI.PettyProjection.mem_smul_wulff line 142
20. lemma OAI.PettyProjection.gauge_wulff_eq_max line 149
21. lemma OAI.PettyProjection.gauge_ae_differentiable_sphere line 168
22. lemma OAI.PettyProjection.Spherical.rotDeriv_comp_scalar line 190
23. lemma OAI.PettyProjection.Spherical.energy_comp_relation line 197
24. lemma OAI.PettyProjection.Spherical.smooth_convex_energy_bound line 216
25. lemma OAI.PettyProjection.Spherical.smooth_convex_curvature line 251
26. lemma OAI.PettyProjection.Spherical.continuous_mean line 271
27. lemma OAI.PettyProjection.Spherical.continuous_variance line 281
28. def OAI.PettyProjection.Spherical.shrinkingBump line 291
29. lemma OAI.PettyProjection.Spherical.seminorm_approximation line 299
30. theorem OAI.PettyProjection.Spherical.seminorm_curvature line 332

    Source documentation

    The nonsmooth curvature inequality, proved by actual even convolution of an arbitrary seminorm. No smoothness, homogeneity of approximants, or assumed spectral interface is required.

    theorem seminorm_curvature {n : ℕ} (hn : 2 ≤ n) [NeZero n]
        (g : Seminorm ℝ (Space n)) {G I : ℝ → ℝ} {b : ℝ}
        (hG : ContDiff ℝ 1 G) (hI : ContDiff ℝ 1 I)
        (hpos : ∀ z, 0 ≤ I z) (hrel : ∀ z, deriv G z ^ 2 = b ^ 2 * deriv I z) :
        (2 * n : ℝ) * variance (fun u : Sphere n => G (g u)) + (2 * n + 8 : ℝ) *
          ‖Q n (toH n (restrictContinuous (G ∘ g) (hG.continuous.comp (seminorm_continuous n g))))‖ ^ 2 ≤
          ((n : ℝ) - 1) * b ^ 2 * mean (fun u : Sphere n => I (g u) * g u) := by
    …

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