OAI/Geometry/ProjectionBodies/ShadowSlices.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PettyProjection.compact_convex_real_interval line 12
2. lemma OAI.PettyProjection.compact_convex_real_add_interval_volume line 18
3. lemma OAI.PettyProjection.compact_fiber line 33
4. lemma OAI.PettyProjection.convex_fiber line 38
5. lemma OAI.PettyProjection.fiber_vertical_add line 46
6. lemma OAI.PettyProjection.fiber_nonempty_iff line 60
7. theorem OAI.PettyProjection.vertical_segment_volume line 67

   Source documentation

   The actual Fubini segment-addition formula in orthogonal product coordinates.

   theorem vertical_segment_volume {K : Set (E × ℝ)} (hK : IsCompact K)
       (hc : Convex ℝ K) {t : ℝ} (ht : 0 ≤ t) :
       volume (K+Prod.mk (0:E) '' Icc (-t) t) =
         volume K+ENNReal.ofReal (2*t)*volume (Prod.fst '' K) := by
   …

8. lemma OAI.PettyProjection.perpendicular_inner line 99
9. def OAI.PettyProjection.shadowCoordLinear line 103

   Source documentation

   Orthogonal coordinates with the last coordinate in a specified unit direction.

   def shadowCoordLinear {n : ℕ} (u : Sphere n) :
       WithLp 2 (perpendicular (u : Space n) × ℝ) →ₗ[ℝ] Space n where
   …

   Mentions: OAI.PettyProjection.perpendicular, OAI.PettyProjection.Space

10. lemma OAI.PettyProjection.shadowCoordLinear_inner line 113
11. lemma OAI.PettyProjection.shadowCoordLinear_surjective line 124
12. def OAI.PettyProjection.shadowCoords line 133
13. lemma OAI.PettyProjection.shadowCoords_apply line 139
14. lemma OAI.PettyProjection.shadowCoords_projection line 142
15. def OAI.PettyProjection.shadowMeasurableEquiv line 152

    Source documentation

    The coordinate change preserves the actual standard Euclidean measures.

    def shadowMeasurableEquiv {n : ℕ} (u : Sphere n) :
        (perpendicular (u : Space n) × ℝ) ≃ᵐ Space n :=
    …

    Mentions: OAI.PettyProjection.perpendicular, OAI.PettyProjection.Space

16. lemma OAI.PettyProjection.shadowMeasurableEquiv_measurePreserving line 156
17. def OAI.PettyProjection.unitSegment line 169
18. lemma OAI.PettyProjection.unitSegment_compact line 172
19. lemma OAI.PettyProjection.unitSegment_nonempty line 175
20. lemma OAI.PettyProjection.unitSegment_convex line 178
21. lemma OAI.PettyProjection.unitSegment_support line 181
22. lemma OAI.PettyProjection.smul_unitSegment line 201
23. def OAI.PettyProjection.shadowContinuousEquiv line 210
24. lemma OAI.PettyProjection.shadowContinuousEquiv_apply line 215
25. lemma OAI.PettyProjection.shadow_preimage_projection line 218
26. lemma OAI.PettyProjection.shadow_preimage_add_segment line 234
27. theorem OAI.PettyProjection.segment_volume line 253

    Source documentation

    Adding a centered segment increases volume by its length times the actual orthogonal shadow volume. No boundary regularity is used.

    theorem segment_volume {n : ℕ} (u : Sphere n) {K : Set (Space n)}
        (hK : IsCompact K) (hc : Convex ℝ K) {t : ℝ} (ht : 0 ≤ t) :
        volume.real (K+t • unitSegment (u : Space n)) =
          volume.real K+2*t*shadowVolume K u := by
    …

    Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.unitSegment, OAI.PettyProjection.shadowVolume

28. theorem OAI.PettyProjection.shadow_gauge_formula line 273

    Source documentation

    Gauge representation of actual orthogonal shadow volume.

    theorem shadow_gauge_formula {n : ℕ} [NeZero n] {K : Set (Space n)}
        (hK : IsCompact K) (hc : Convex ℝ K) (h0 : K ∈ 𝓝 (0 : Space n)) (u : Sphere n) :
        2*shadowVolume K u = n*kappa n*mean (fun v : Sphere n =>
          (gauge K (v : Space n))⁻¹^n*|⟪∇ (gauge K) (v : Space n),(u : Space n)⟫|) := by
    …

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