OAI/Geometry/ProjectionBodies/VariationalRepresentation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PettyProjection.RelativeGauge.normalized_representation line 15

   Source documentation

   Actual Euler equation for the normalized variational optimizer. The test is only continuous, even and degree-one homogeneous, not assumed convex.

   theorem normalized_representation {μ : Measure (Space n)}
       (hμ : Integrable (fun x : Space n => ‖x‖) μ)
       (hq : ∀ x : Space n,x≠0 → 0<cosineSeminorm μ hμ x) (b : Bool)
       (g : RelativeGauge (⊤ : Submodule ℝ (Space n))) (hgn : supportFunctional μ g.body=1)
       (hmin : ∀ q : RelativeGauge (⊤ : Submodule ℝ (Space n)),supportFunctional μ q.body=1 →
         objective b g.toSeminorm≤objective b q.toSeminorm)
       (φ : Space n → ℝ) (hφ : Continuous φ) (heven : ∀ x,φ (-x)=φ x)
       (hh : ∀ a : ℝ,0<a → ∀ x,φ (a • x)=a*φ x) :
       (∫ x,φ x ∂μ)*(if b then 1 else objective false g.toSeminorm)=
         mean (fun u : Sphere n => (if b then 1 else g u)*φ (∇ (fun x => g x) (u:Space n))) := by
   …

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

2. lemma OAI.PettyProjection.normalizedVolume_pos line 93
3. lemma OAI.PettyProjection.normalizedVolume_pow line 97
4. lemma OAI.PettyProjection.normalizedVolume_smul line 102
5. lemma OAI.PettyProjection.RelativeGauge.top_pos line 111
6. lemma OAI.PettyProjection.RelativeGauge.top_interior line 115
7. def OAI.PettyProjection.RelativeGauge.volumeNormalize line 118
8. lemma OAI.PettyProjection.RelativeGauge.volumeNormalize_body_volume line 122
9. lemma OAI.PettyProjection.RelativeGauge.volumeNormalize_moment line 129
10. lemma OAI.PettyProjection.RelativeGauge.full_body_of_sphere_one line 138
11. def OAI.PettyProjection.RelativeGauge.fullOfRange line 155
12. lemma OAI.PettyProjection.RelativeGauge.fullOfRange_body line 162
13. def OAI.PettyProjection.regime line 176
14. lemma OAI.PettyProjection.exponent_pos line 177
15. lemma OAI.PettyProjection.RelativeGauge.scale_field_ae line 183
16. lemma OAI.PettyProjection.RelativeGauge.scale_moment line 202
17. lemma OAI.PettyProjection.RelativeGauge.minimizer_field_representation line 207
18. lemma OAI.PettyProjection.RelativeGauge.scaled_field_representation line 234