OAI/Geometry/ProjectionBodies/SliceTransport.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PettyProjection.transport_scalar line 13

   Source documentation

   The strict scalar inequality in the slice transport proof of Brunn--Minkowski. The variables p,q are the positive slice-volume roots.

   lemma transport_scalar {m : ℕ} (hm : 0 < m) {a b p q : ℝ}
       (ha : 0 < a) (hb : 0 < b) (hab : a+b=1) (hp : 0 < p) (hq : 0 < q) :
       1 ≤ (a*p+b*q)^m*(a/(p^m)+b/(q^m)) ∧
         ((a*p+b*q)^m*(a/(p^m)+b/(q^m))=1 ↔ p=q) := by
   …

2. theorem OAI.PettyProjection.exists_interval_quantile line 64

   Source documentation

   The inverse cumulative mass coordinate on a compact interval. Zero density at the two endpoints is allowed; the derivative is needed only in the interior.

   theorem exists_interval_quantile {l r : ℝ} (hlr : l < r) {f : ℝ → ℝ}
       (hf : ContinuousOn f (Ioo l r)) (hI : IntervalIntegrable f volume l r)
       (hpos : ∀ x ∈ Ioo l r, 0 < f x)
       (hmass : (∫ x in l..r, f x)=1) :
       ∃ Q : ℝ → ℝ, Continuous Q ∧ Q 0=l ∧ Q 1=r ∧
         (∀ s ∈ Icc (0:ℝ) 1, Q s ∈ Icc l r) ∧
         (∀ s ∈ Ioo (0:ℝ) 1, Q s ∈ Ioo l r ∧
           HasDerivAt Q (f (Q s))⁻¹ s) := by
   …

3. theorem OAI.PettyProjection.slice_transport line 134

   Source documentation

   The analytic step of the slice proof. All three functions here are actual slice densities when this result is applied to convex bodies.

   theorem slice_transport {m : ℕ} (hm : 0 < m) {a b l r L R : ℝ}
       (ha : 0 < a) (hb : 0 < b) (hab : a+b=1) (hlr : l<r) (hLR : L<R)
       {f g h : ℝ → ℝ}
       (hf : ContinuousOn f (Ioo l r)) (hg : ContinuousOn g (Ioo L R))
       (hfi : IntervalIntegrable f volume l r) (hgi : IntervalIntegrable g volume L R)
       (hfp : ∀ x ∈ Ioo l r, 0<f x) (hgp : ∀ x ∈ Ioo L R, 0<g x)
       (hfI : (∫ x in l..r, f x)=1) (hgI : (∫ x in L..R, g x)=1)
       (hhi : IntervalIntegrable h volume (a*l+b*L) (a*r+b*R))
       (hbound : ∀ x ∈ Ioo l r, ∀ y ∈ Ioo L R,
         (a*(f x)^((m:ℝ)⁻¹)+b*(g y)^((m:ℝ)⁻¹))^m ≤ h (a*x+b*y)) :
       1 ≤ ∫ z in (a*l+b*L)..(a*r+b*R), h z := by
   …

4. def OAI.PettyProjection.horizontalSlice line 203
5. lemma OAI.PettyProjection.horizontalSlice_compact line 206
6. lemma OAI.PettyProjection.horizontalSlice_convex line 211
7. lemma OAI.PettyProjection.horizontalSlice_nonempty_iff line 219
8. lemma OAI.PettyProjection.horizontalSlice_minkowski_subset line 225
9. lemma OAI.PettyProjection.horizontalSlice_combo_subset line 231
10. lemma OAI.PettyProjection.interior_slice_of_interior line 239
11. lemma OAI.PettyProjection.interior_point_at_height line 245

    Source documentation

    A projection point strictly between two attained heights is a height of an interior point. No smoothness of the convex body is imposed.

    lemma interior_point_at_height {K : Set (E × ℝ)} (hK : Convex ℝ K)
        (hi : (interior K).Nonempty) {l r s : ℝ}
        (hl : l ∈ Prod.snd '' K) (hr : r ∈ Prod.snd '' K) (hs : s ∈ Ioo l r) :
        ∃ x : E, (x,s) ∈ interior K := by
    …

12. lemma OAI.PettyProjection.horizontalSlice_interior_nonempty line 283
13. lemma OAI.PettyProjection.vertical_projection_interval line 290
14. def OAI.PettyProjection.sliceDensity line 316
15. lemma OAI.PettyProjection.sliceDensity_nonneg line 320
16. lemma OAI.PettyProjection.sliceDensity_pos line 323
17. lemma OAI.PettyProjection.sliceDensity_zero_of_notMem line 333
18. lemma OAI.PettyProjection.sliceDensity_indicator_integral line 340
19. lemma OAI.PettyProjection.sliceDensity_integrable line 351
20. lemma OAI.PettyProjection.sliceDensity_integral line 358
21. lemma OAI.PettyProjection.sliceDensity_interval_integral line 368