OAI/Geometry/ProjectionBodies/WulffVariation.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PettyProjection.support_gradient_of_active line 13
2. lemma OAI.PettyProjection.wulff_gradient_of_active line 34
3. lemma OAI.PettyProjection.wulff_active_unique line 45
4. lemma OAI.PettyProjection.selected_max_tendsto line 67

   Source documentation

   Convergence of maximizers at a unique maximum, with a compact parameter space and joint continuity only at the limiting parameter.

   lemma selected_max_tendsto {U : Type uU} [TopologicalSpace U] [CompactSpace U]
       {f : ℝ → U → ℝ} {a : ℝ → U} {u₀ : U}
       (hc : ∀ u : U, ContinuousAt (fun p : ℝ × U => f p.1 p.2) (0,u))
       (hm : ∀ᶠ t in 𝓝 (0 : ℝ), ∀ u, f t u ≤ f t (a t))
       (hu : ∀ u, (∀ v, f 0 v ≤ f 0 u) → u = u₀) :
       Tendsto a (𝓝 0) (𝓝 u₀) := by
   …

5. lemma OAI.PettyProjection.quotient_bounds line 85
6. lemma OAI.PettyProjection.hasDerivAt_selected_max line 98

   Source documentation

   Envelope differentiation from an exact continuous difference quotient. The statement does not require a smooth boundary or a smooth maximizer.

   lemma hasDerivAt_selected_max {U : Type uU} [TopologicalSpace U] [CompactSpace U]
       {f d : ℝ → U → ℝ} {q : ℝ → ℝ} {a : ℝ → U} {u₀ : U}
       (hc : ∀ u : U, ContinuousAt (fun p : ℝ × U => f p.1 p.2) (0,u))
       (hd : ContinuousAt (fun p : ℝ × U => d p.1 p.2) (0,u₀))
       (hq : ∀ᶠ t in 𝓝 (0 : ℝ), q t = f t (a t) ∧ ∀ u, f t u ≤ q t)
       (hq₀ : q 0 = f 0 u₀) (hm₀ : ∀ u, f 0 u ≤ q 0)
       (hu : ∀ u, (∀ v, f 0 v ≤ f 0 u) → u = u₀)
       (he : ∀ᶠ t in 𝓝 (0 : ℝ), ∀ u, f t u-f 0 u = t*d t u) :
       HasDerivAt q (d 0 u₀) 0 := by
   …

7. lemma OAI.PettyProjection.positive_constraints_eventually line 144
8. lemma OAI.PettyProjection.positive_constraints_nhds line 165
9. lemma OAI.PettyProjection.wulff_derivative_active line 171
10. theorem OAI.PettyProjection.wulff_derivative line 229

    Source documentation

    Wulff variation against an actual continuous positively homogeneous test. No symmetry or boundary smoothness is assumed.

    theorem wulff_derivative {n : ℕ} [NeZero n] (s : C(Sphere n,ℝ))
        (hs : ∀ u, 0 < s u) (φ : Space n → ℝ) (hφ : Continuous φ)
        (hh : ∀ (a : ℝ), 0 < a → ∀ x, φ (a • x) = a*φ x)
        {x : Space n} (hd : DifferentiableAt ℝ (gauge (wulff s)) x) :
        HasDerivAt (fun t : ℝ => gauge (wulff (s+t • (⟨fun u : Sphere n => φ u,
          hφ.comp continuous_subtype_val⟩ : C(Sphere n,ℝ)))) x)
          (-(gauge (wulff s) x)*φ (∇ (gauge (wulff s)) x)) 0 := by
    …

    Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.wulff

11. lemma OAI.PettyProjection.kappa_pos line 253
12. lemma OAI.PettyProjection.surface_real_univ line 258
13. lemma OAI.PettyProjection.gauge_volume_lintegral line 266

    Source documentation

    Polar integration of an arbitrary convex neighborhood of zero; the body need not be symmetric or have a smooth boundary.

    lemma gauge_volume_lintegral {n : ℕ} [NeZero n] {K : Set (Space n)}
        (hc : Convex ℝ K) (h0 : K ∈ 𝓝 (0 : Space n))
        (hp : ∀ u : Sphere n, 0 < gauge K (u : Space n)) :
        volume K = ∫⁻ u : Sphere n, ENNReal.ofReal ((gauge K (u : Space n))⁻¹ ^ n / n)
          ∂surface n := by
    …

    Mentions: OAI.PettyProjection.Space

14. lemma OAI.PettyProjection.gauge_volume line 309
15. lemma OAI.PettyProjection.wulff_volume line 327
16. lemma OAI.PettyProjection.wulff_sphere_gauge_bounds line 343
17. lemma OAI.PettyProjection.quotient_perturb_bound line 361
18. lemma OAI.PettyProjection.wulff_gauge_param_sub_le line 376
19. lemma OAI.PettyProjection.wulff_gauge_param_lipschitz line 394
20. lemma OAI.PettyProjection.measurable_gradient line 417
21. lemma OAI.PettyProjection.wulff_invpow_param_lipschitz line 420
22. lemma OAI.PettyProjection.wulff_invpow_derivative line 438
23. theorem OAI.PettyProjection.wulff_volume_derivative line 462

    Source documentation

    Actual two-sided first variation in positive Wulff constraints. This is valid for arbitrary continuous degree-one tests, not only support functions.

    theorem wulff_volume_derivative {n : ℕ} [NeZero n] (s : C(Sphere n,ℝ))
        (hs : ∀ u,0 < s u) (φ : Space n → ℝ) (hφ : Continuous φ)
        (hh : ∀ (a : ℝ),0 < a → ∀ x,φ (a • x)=a*φ x) :
        HasDerivAt (fun t : ℝ => volume.real (wulff ⇑(s+t • (⟨fun u : Sphere n => φ u,
          hφ.comp continuous_subtype_val⟩ : C(Sphere n,ℝ)))))
          (n*kappa n*mean (fun u : Sphere n => (gauge (wulff s) (u : Space n))⁻¹^n*
            φ (∇ (gauge (wulff s)) (u : Space n)))) 0 := by
    …

    Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.wulff, OAI.PettyProjection.kappa

24. lemma OAI.PettyProjection.support_smul_set line 519
25. lemma OAI.PettyProjection.support_pos_of_nhds line 532
26. theorem OAI.PettyProjection.minkowski_volume_derivative line 545

    Source documentation

    First-variation identity for actual Minkowski addition; the added set is allowed to have any dimension.

    theorem minkowski_volume_derivative {n : ℕ} [NeZero n] {K M : Set (Space n)}
        (hK : IsCompact K) (hcK : Convex ℝ K) (h0 : K ∈ 𝓝 (0 : Space n))
        (hM : IsCompact M) (hcM : Convex ℝ M) (hMn : M.Nonempty) :
        HasDerivWithinAt (fun t : ℝ => volume.real (K+t • M))
          (n*kappa n*mean (fun u : Sphere n => (gauge K (u : Space n))⁻¹^n*
            support M (∇ (gauge K) (u : Space n)))) (Ici 0) 0 := by
    …

    Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.kappa, OAI.PettyProjection.support