OAI/Geometry/ProjectionBodies/Homothety.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PettyProjection.quantile_first_moment line 11
2. theorem OAI.PettyProjection.slice_transport_equality line 32

   Source documentation

   Equality in slice transport forces the two full marginal distributions to be translates. In particular both projection endpoints differ by the difference of their first moments.

   theorem slice_transport_equality {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))
       (hI : (∫ z in (a*l+b*L)..(a*r+b*R), h z)=1) :
       l-L=(∫ x in l..r, x*f x)-(∫ y in L..R, y*g y) ∧
   …

3. lemma OAI.PettyProjection.sliceDensity_moment_indicator line 152
4. lemma OAI.PettyProjection.sliceDensity_moment_integrable line 163
5. lemma OAI.PettyProjection.sliceDensity_moment line 170
6. lemma OAI.PettyProjection.sliceDensity_interval_moment line 179
7. theorem OAI.PettyProjection.brunnMinkowski_product_unit_equality line 203

   Source documentation

   Equality in the actual product-body step identifies both extreme heights with the difference of the (unit-volume) vertical first moments.

   theorem brunnMinkowski_product_unit_equality {m : ℕ} (hm0 : 0 < m) (hm : BrunnMinkowskiRoot E m)
       {K M : Set (E × ℝ)} (hK : IsCompact K) (hcK : Convex ℝ K)
       (hiK : (interior K).Nonempty) (hM : IsCompact M) (hcM : Convex ℝ M)
       (hiM : (interior M).Nonempty) (hvK : volume.real K=1) (hvM : volume.real M=1)
       {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a+b=1)
       (hvC : volume.real (a • K+b • M)=1)
       {l r L R : ℝ} (hlr : l<r) (hLR : L<R)
       (hpr : Prod.snd '' K=Icc l r) (hPR : Prod.snd '' M=Icc L R) :
       l-L=(∫ x in K, x.2)-(∫ x in M, x.2) ∧
       r-R=(∫ x in K, x.2)-(∫ x in M, x.2) := by
   …

   Mentions: OAI.PettyProjection.BrunnMinkowskiRoot

8. def OAI.PettyProjection.firstMoment line 265

   Source documentation

   The unnormalized Euclidean first moment. It is the barycenter for unit volume bodies, the only place where it is used below.

   def firstMoment {n : ℕ} (K : Set (Space n)) : Space n := ∫ x in K, x

   Mentions: OAI.PettyProjection.Space

9. lemma OAI.PettyProjection.shadowContinuousEquiv_inner line 267
10. lemma OAI.PettyProjection.shadow_vertical_image line 274
11. lemma OAI.PettyProjection.shadow_firstMoment line 284
12. lemma OAI.PettyProjection.perpendicular_finrank line 293
13. theorem OAI.PettyProjection.brunnMinkowski_unit_support_equality line 305

    Source documentation

    Equality for an intermediate Minkowski combination of unit-volume bodies identifies every directional support difference with the first-moment shift.

    theorem brunnMinkowski_unit_support_equality {n : ℕ} (hn : 2 ≤ n)
        {K M : Set (Space n)} (hK : IsCompact K) (hcK : Convex ℝ K)
        (hiK : (interior K).Nonempty) (hM : IsCompact M) (hcM : Convex ℝ M)
        (hiM : (interior M).Nonempty) (hvK : volume.real K=1) (hvM : volume.real M=1)
        {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a+b=1)
        (hvC : volume.real (a • K+b • M)=1) (u : Sphere n) :
        support K u-support M u=⟪(u : Space n),firstMoment K-firstMoment M⟫ := by
    …

    Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.support, OAI.PettyProjection.firstMoment

14. lemma OAI.PettyProjection.support_translate line 348
15. theorem OAI.PettyProjection.brunnMinkowski_unit_equality line 362

    Source documentation

    The unrestricted translated-body equality case of the unit-volume Brunn--Minkowski inequality (no origin symmetry or boundary regularity).

    theorem brunnMinkowski_unit_equality {n : ℕ} (hn : 2 ≤ n)
        {K M : Set (Space n)} (hK : IsCompact K) (hcK : Convex ℝ K)
        (hiK : (interior K).Nonempty) (hM : IsCompact M) (hcM : Convex ℝ M)
        (hiM : (interior M).Nonempty) (hvK : volume.real K=1) (hvM : volume.real M=1)
        {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a+b=1)
        (hvC : volume.real (a • K+b • M)=1) :
        K=(fun x => firstMoment K-firstMoment M+x) '' M := by
    …

    Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.firstMoment

16. def OAI.PettyProjection.volumeRoot line 395
17. lemma OAI.PettyProjection.volumeRoot_pos line 397
18. lemma OAI.PettyProjection.volumeRoot_pow line 401
19. lemma OAI.PettyProjection.volumeRoot_smul line 405
20. lemma OAI.PettyProjection.interior_add_nonempty_left line 413
21. theorem OAI.PettyProjection.brunnMinkowski_add line 422

    Source documentation

    The homogeneous, additive form of Brunn--Minkowski.

    theorem brunnMinkowski_add {n : ℕ} (hn : 0 < n)
        {K M : Set (Space n)} (hK : IsCompact K) (hcK : Convex ℝ K)
        (hiK : (interior K).Nonempty) (hM : IsCompact M) (hcM : Convex ℝ M)
        (hiM : (interior M).Nonempty) :
        volumeRoot K+volumeRoot M ≤ volumeRoot (K+M) := by
    …

    Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.volumeRoot

22. theorem OAI.PettyProjection.brunnMinkowski_add_equality line 434

    Source documentation

    Equality in the homogeneous additive form, retaining arbitrary translation.

    theorem brunnMinkowski_add_equality {n : ℕ} (hn : 2 ≤ n)
        {K M : Set (Space n)} (hK : IsCompact K) (hcK : Convex ℝ K)
        (hiK : (interior K).Nonempty) (hM : IsCompact M) (hcM : Convex ℝ M)
        (hiM : (interior M).Nonempty)
        (hv : volumeRoot (K+M)=volumeRoot K+volumeRoot M) :
        ∃ z : Space n, ∃ c : ℝ, 0 < c ∧ K=(fun x => z+c • x) '' M := by
    …

    Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.volumeRoot

23. lemma OAI.PettyProjection.minkowski_parameter_combo line 487
24. lemma OAI.PettyProjection.minkowski_volumeRoot_concave line 494
25. lemma OAI.PettyProjection.volumeRoot_diff_factor line 508
26. theorem OAI.PettyProjection.minkowski_derivative_bound_equality line 521

    Source documentation

    The sharp first-variation inequality together with its global translated homothety equality implication, derived from actual Brunn--Minkowski concavity.

    theorem minkowski_derivative_bound_equality {n : ℕ} (hn : 2 ≤ n)
        {K M : Set (Space n)} (hK : IsCompact K) (hcK : Convex ℝ K)
        (hiK : (interior K).Nonempty) (hM : IsCompact M) (hcM : Convex ℝ M)
        (hiM : (interior M).Nonempty) {d : ℝ}
        (hd : HasDerivWithinAt (fun t : ℝ => volume.real (K+t • M)) d (Ici 0) 0) :
        (n:ℝ)*volumeRoot K^(n-1)*volumeRoot M ≤ d ∧
          (d=(n:ℝ)*volumeRoot K^(n-1)*volumeRoot M →
            ∃ z : Space n, ∃ c : ℝ, 0 < c ∧ K=(fun x => z+c • x) '' M) := by
    …

    Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.volumeRoot