OAI/Geometry/ProjectionBodies/BilinearEquality.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PettyProjection.RelativeGauge.scale_momentField line 14
2. lemma OAI.PettyProjection.RelativeGauge.volumeNormalize_harmonic line 30
3. lemma OAI.PettyProjection.RelativeGauge.volumeNormalize_representation line 38
4. lemma OAI.PettyProjection.normalizedVolume_of_volume line 63
5. lemma OAI.PettyProjection.cosine_equiv_pos line 67
6. theorem OAI.PettyProjection.measure_bilinear line 78

   Source documentation

   The genuine bilinear inequality, with its global rigidity consequence. The hypotheses are the support-functional bounds supplied by Brunn--Minkowski, not the desired projection-volume conclusion.

   theorem measure_bilinear {n : ℕ} (hn : 4≤ n) [NeZero n] {μ ν : Measure (Space n)}
       (hμ : Integrable (fun x : Space n => ‖x‖) μ)
       (hν : Integrable (fun x : Space n => ‖x‖) ν)
       (hqμ : ∀ x : Space n,x≠0 → 0< cosineSeminorm μ hμ x)
       (hqν : ∀ x : Space n,x≠0 → 0< cosineSeminorm ν hν x)
       (hbμ : ∀ M : Set (Space n),IsConvexBody M → normalizedVolume M≤ supportFunctional μ M)
       (hbν : ∀ M : Set (Space n),IsConvexBody M → normalizedVolume M≤ supportFunctional ν M) :
       cosineConstant n≤ measurePair μ ν ∧
         (measurePair μ ν=cosineConstant n →
           ∃ T : Space n ≃L[ℝ] Space n,supportFunctional μ (T '' unitBall n)=normalizedVolume (T '' unitBall n)) := by
   …

   Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.cosineSeminorm, OAI.PettyProjection.IsConvexBody, OAI.PettyProjection.normalizedVolume, OAI.PettyProjection.supportFunctional, OAI.PettyProjection.measurePair, OAI.PettyProjection.unitBall

7. lemma OAI.PettyProjection.gaugeMeasure_norm_integrable line 159
8. lemma OAI.PettyProjection.gaugeMeasure_cosine_pos line 164
9. def OAI.PettyProjection.projectionSeminorm line 179
10. lemma OAI.PettyProjection.projectionSeminorm_unit line 188
11. lemma OAI.PettyProjection.projectionSeminorm_pos line 194
12. lemma OAI.PettyProjection.projectionBody_eq_wulff line 199
13. lemma OAI.PettyProjection.projectionBody_body line 213
14. lemma OAI.PettyProjection.projectionBody_nhds line 219
15. lemma OAI.PettyProjection.projectionBody_support line 225
16. lemma OAI.PettyProjection.projectionBody_support_unit line 231
17. lemma OAI.PettyProjection.unitBall_body line 247
18. lemma OAI.PettyProjection.unitBall_nhds line 251
19. lemma OAI.PettyProjection.shadowVolume_unitBall line 254
20. lemma OAI.PettyProjection.gradient_norm_unit line 278
21. lemma OAI.PettyProjection.ball_cosine_constant line 292