OAI/Geometry/ProjectionBodies/VariationalMinimizers.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PettyProjection.RelativeGauge.exists_normalized line 13
2. theorem OAI.PettyProjection.RelativeGauge.exists_minimizer line 23

   Source documentation

   The actual fixed-subspace variational minimizer, including singular V.

   theorem exists_minimizer {μ : Measure (Space n)}
       (hμ : Integrable (fun x : Space n => ‖x‖) μ) (hV : V≠⊥)
       (hq : ∀ x∈V,x≠0 → 0<cosineSeminorm μ hμ x) (b : Bool) :
       ∃ g : RelativeGauge V,supportFunctional μ g.body=1 ∧
         ∀ f : RelativeGauge V,supportFunctional μ f.body=1 →
           Spherical.objective b g.toSeminorm≤Spherical.objective b f.toSeminorm := by
   …

   Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.cosineSeminorm, OAI.PettyProjection.RelativeGauge, OAI.PettyProjection.supportFunctional, OAI.PettyProjection.Spherical.objective

3. def OAI.PettyProjection.RelativeGauge.midBody line 68
4. lemma OAI.PettyProjection.RelativeGauge.midBody_compact line 69
5. lemma OAI.PettyProjection.RelativeGauge.midBody_convex line 71
6. lemma OAI.PettyProjection.RelativeGauge.midBody_balanced line 73
7. lemma OAI.PettyProjection.RelativeGauge.midBody_sub line 75
8. lemma OAI.PettyProjection.RelativeGauge.midBody_inner line 78
9. def OAI.PettyProjection.RelativeGauge.midpoint line 86
10. lemma OAI.PettyProjection.RelativeGauge.body_midpoint line 88
11. lemma OAI.PettyProjection.RelativeGauge.functional_midpoint line 90
12. lemma OAI.PettyProjection.RelativeGauge.midpoint_harmonic line 97
13. lemma OAI.PettyProjection.Spherical.harmonic_objective line 126
14. lemma OAI.PettyProjection.RelativeGauge.ext line 170
15. lemma OAI.PettyProjection.RelativeGauge.midpoint_objective line 173
16. lemma OAI.PettyProjection.RelativeGauge.minimizer_unique line 210
17. lemma OAI.PettyProjection.objective_param_lipschitz line 233
18. lemma OAI.PettyProjection.objectiveIntegrand_continuousOn line 251
19. lemma OAI.PettyProjection.objective_gauge_derivative line 256
20. theorem OAI.PettyProjection.wulff_objective_derivative line 275

    Source documentation

    Two-sided first variation of both variational objectives, with no smoothness assumption on the optimizer.

    theorem wulff_objective_derivative {n : ℕ} [NeZero n] (b : Bool) (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 : ℝ => mean (fun u : Sphere n => objectiveIntegrand b
          (gauge (wulff ⇑(s+t • (⟨fun v : Sphere n => φ v,
            hφ.comp continuous_subtype_val⟩ : C(Sphere n,ℝ)))) (u:Space n))))
          (-mean (fun u : Sphere n => (if b then 1 else gauge (wulff s) (u:Space n))*
            φ (∇ (gauge (wulff s)) (u:Space n)))) 0 := by
    …

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

21. lemma OAI.PettyProjection.support_even line 324
22. lemma OAI.PettyProjection.wulff_balanced line 336
23. lemma OAI.PettyProjection.RelativeGauge.top_body line 347
24. lemma OAI.PettyProjection.RelativeGauge.top_nhds line 349
25. lemma OAI.PettyProjection.RelativeGauge.top_gauge line 351
26. lemma OAI.PettyProjection.RelativeGauge.full_inner line 353
27. def OAI.PettyProjection.RelativeGauge.ofFullBody line 359
28. lemma OAI.PettyProjection.RelativeGauge.body_ofFullBody line 362
29. lemma OAI.PettyProjection.RelativeGauge.ofFullBody_apply line 365
30. lemma OAI.PettyProjection.homogeneous_integrable line 371
31. lemma OAI.PettyProjection.seminorm_supporting_vector line 404

    Source documentation

    Hahn--Banach attainment for the actual Wulff body of a seminorm.

    lemma seminorm_supporting_vector {n : ℕ} (q : Seminorm ℝ (Space n)) (u : Sphere n) :
        ∃ z : Space n,(∀ x : Space n,|⟪x,z⟫|≤q x) ∧ ⟪(u:Space n),z⟫=q u := by
    …

    Mentions: OAI.PettyProjection.Space

32. lemma OAI.PettyProjection.support_wulff_seminorm_unit line 425
33. lemma OAI.PettyProjection.support_wulff_seminorm line 438
34. lemma OAI.PettyProjection.homogeneous_zero line 464
35. lemma OAI.PettyProjection.support_wulff_bound line 470
36. lemma OAI.PettyProjection.functional_wulff_bound line 500
37. lemma OAI.PettyProjection.RelativeGauge.minimizer_scaled_lower line 517