OAI/Analysis/Brenier/CellGeometry.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem358.CellGeometry.closedCell line 16

   Source documentation

   The closed cell of one affine branch, including ties.

   def closedCell (K : Set (E d)) (y : ι → E d) (c : ι → ℝ) (i : ι) : Set (E d) :=
   …

2. theorem OAI.Problem358.CellGeometry.closedCell_subset line 19
3. theorem OAI.Problem358.CellGeometry.isClosed_closedCell line 22
4. theorem OAI.Problem358.CellGeometry.isCompact_closedCell line 33
5. theorem OAI.Problem358.CellGeometry.convex_closedCell line 38
6. theorem OAI.Problem358.CellGeometry.exists_mem_closedCell line 49
7. theorem OAI.Problem358.CellGeometry.iUnion_closedCell line 56
8. theorem OAI.Problem358.CellGeometry.exists_strict_active_interior line 70

   Source documentation

   Positive-volume cells have strictly active points in the interior, once affine ties have been removed as a null set.

   theorem exists_strict_active_interior {K : Set (E d)}
       (hconv : Convex ℝ K) (y : ι → E d) (c : ι → ℝ) (i : ι)
       (hpos : volume (closedCell K y c i) ≠ 0)
       (hties : ∀ᵐ x ∂volume, ∀ j, j ≠ i →
         inner ℝ x (y j) + c j ≠ inner ℝ x (y i) + c i) :
       ∃ x ∈ interior K, ∀ j, j ≠ i →
         inner ℝ x (y j) + c j < inner ℝ x (y i) + c i := by
   …

   Mentions: OAI.Problem358.CellGeometry.closedCell

9. theorem OAI.Problem358.CellGeometry.combo_mem_closedCell line 89

   Source documentation

   Convex interpolation of the intercepts and source points remains in the same cell.

   theorem combo_mem_closedCell {K : Set (E d)} (hK : Convex ℝ K)
       (y : ι → E d) (c e : ι → ℝ) (i : ι) {x z : E d}
       (hx : x ∈ closedCell K y c i) (hz : z ∈ closedCell K y e i)
       {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
       a • x + b • z ∈ closedCell K y (fun j => a * c j + b * e j) i := by
   …

   Mentions: OAI.Problem358.CellGeometry.closedCell

10. theorem OAI.Problem358.CellGeometry.midpoint_mem_closedCell line 102

    Source documentation

    The opposite-intercept midpoint inclusion used in the moment estimate.

    theorem midpoint_mem_closedCell {K : Set (E d)} (hK : Convex ℝ K)
        (y : ι → E d) (c q : ι → ℝ) (i : ι) (s : ℝ) {x z : E d}
        (hx : x ∈ closedCell K y (fun j => c j - s * q j) i)
        (hz : z ∈ closedCell K y (fun j => c j + s * q j) i) :
        (1 / 2 : ℝ) • x + (1 / 2 : ℝ) • z ∈ closedCell K y c i := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

11. theorem OAI.Problem358.CellGeometry.exists_affine_equality_interior line 118

    Source documentation

    An affine equality plane separating two strictly active interior points meets the interior of the convex source.

    theorem exists_affine_equality_interior {K : Set (E d)} (hK : Convex ℝ K)
        {y z : E d} {c e : ℝ} {p q : E d}
        (hp : p ∈ interior K) (hq : q ∈ interior K)
        (hp_lt : inner ℝ p y + c < inner ℝ p z + e)
        (hq_lt : inner ℝ q z + e < inner ℝ q y + c) :
        ∃ x ∈ interior K, inner ℝ x y + c = inner ℝ x z + e := by
    …

12. theorem OAI.Problem358.CellGeometry.pairwise_aedisjoint_closedCell line 149

    Source documentation

    Distinct-site closed cells overlap only along null affine tie planes.

    theorem pairwise_aedisjoint_closedCell {ρ : Measure (E d)} (hρ : ρ ≪ volume)
        (K : Set (E d)) (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y) :
        Pairwise (fun i j => AEDisjoint ρ (closedCell K y c i) (closedCell K y c j)) := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

13. theorem OAI.Problem358.CellGeometry.sum_measure_closedCell line 162

    Source documentation

    The closed cells form a finite partition for all measures absolutely continuous with respect to volume.

    theorem sum_measure_closedCell [Fintype ι] [Nonempty ι]
        {ρ : Measure (E d)} (hρ : ρ ≪ volume) {K : Set (E d)} (hK : IsClosed K)
        (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y) :
        (∑ i, ρ (closedCell K y c i)) = ρ K := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

14. theorem OAI.Problem358.CellGeometry.sum_integral_closedCell line 171

    Source documentation

    Integrable functions can be summed cellwise despite the shared boundary faces.

    theorem sum_integral_closedCell [Fintype ι] [Nonempty ι]
        {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
        {ρ : Measure (E d)} (hρ : ρ ≪ volume) {K : Set (E d)} (hK : IsClosed K)
        (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
        {f : E d → V} (hf : IntegrableOn f K ρ) :
        (∑ i, ∫ x in closedCell K y c i, f x ∂ρ) = ∫ x in K, f x ∂ρ := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

15. theorem OAI.Problem358.CellGeometry.sum_real_measure_closedCell line 185

    Source documentation

    Real-valued cell masses also add to the total source mass.

    theorem sum_real_measure_closedCell [Fintype ι] [Nonempty ι]
        {ρ : Measure (E d)} [IsFiniteMeasure ρ] (hρ : ρ ≪ volume)
        {K : Set (E d)} (hK : IsClosed K)
        (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y) :
        (∑ i, ρ.real (closedCell K y c i)) = ρ.real K := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

16. theorem OAI.Problem358.CellGeometry.exists_strict_active_interior_of_injective line 196

    Source documentation

    Injective sites discharge the null-tie premise in strict activation.

    theorem exists_strict_active_interior_of_injective [Countable ι]
        {K : Set (E d)} (hK : Convex ℝ K) (y : ι → E d) (c : ι → ℝ)
        (hy : Function.Injective y) (i : ι) (hpos : volume (closedCell K y c i) ≠ 0) :
        ∃ x ∈ interior K, ∀ j, j ≠ i →
          inner ℝ x (y j) + c j < inner ℝ x (y i) + c i := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

17. theorem OAI.Problem358.CellGeometry.exists_strict_active_interior_of_mass line 208

    Source documentation

    Positive cell mass for an absolutely continuous source already guarantees a strictly active interior point.

    theorem exists_strict_active_interior_of_mass [Countable ι]
        {ρ : Measure (E d)} (hρ : ρ ≪ volume) {K : Set (E d)} (hK : Convex ℝ K)
        (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
        (i : ι) (hpos : ρ (closedCell K y c i) ≠ 0) :
        ∃ x ∈ interior K, ∀ j, j ≠ i →
          inner ℝ x (y j) + c j < inner ℝ x (y i) + c i := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

18. theorem OAI.Problem358.CellGeometry.exists_equality_interior_of_positive_cells line 218

    Source documentation

    Every equality plane between positive-mass cells cuts the interior of the source.

    theorem exists_equality_interior_of_positive_cells [Countable ι]
        {ρ : Measure (E d)} (hρ : ρ ≪ volume) {K : Set (E d)} (hK : Convex ℝ K)
        (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
        {i j : ι} (hij : i ≠ j)
        (hi : ρ (closedCell K y c i) ≠ 0) (hj : ρ (closedCell K y c j) ≠ 0) :
        ∃ x ∈ interior K, inner ℝ x (y i) + c i = inner ℝ x (y j) + c j := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

19. theorem OAI.Problem358.CellGeometry.ae_fiber_eq_closedCell line 244

    Source documentation

    With distinct slopes, any maximizing index selects the closed affine cell almost everywhere. No measurability of the supplied selector is required.

    theorem ae_fiber_eq_closedCell [Countable ι]
        {K : Set (E d)} (hK : MeasurableSet K)
        (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
        (k : E d → ι)
        (hk : ∀ᵐ x ∂uniformMeasure K, ∀ j,
          ⟪x, y j⟫ + c j ≤ ⟪x, y (k x)⟫ + c (k x)) (i : ι) :
        {x | k x = i} =ᵐ[uniformMeasure K] closedCell K y c i := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

20. theorem OAI.Problem358.CellGeometry.measure_fiber_eq_closedCell line 262

    Source documentation

    Closed-cell masses are exactly the masses of any maximizing selector.

    theorem measure_fiber_eq_closedCell [Countable ι]
        {K : Set (E d)} (hK : MeasurableSet K)
        (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
        (k : E d → ι)
        (hk : ∀ᵐ x ∂uniformMeasure K, ∀ j,
          ⟪x, y j⟫ + c j ≤ ⟪x, y (k x)⟫ + c (k x)) (i : ι) :
        uniformMeasure K {x | k x = i} =
          uniformMeasure K (closedCell K y c i) :=
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

21. theorem OAI.Problem358.CellGeometry.real_fiber_eq_closedCell line 273

    Source documentation

    The real-valued mass form used in the moving-potential energy estimate.

    theorem real_fiber_eq_closedCell [Countable ι]
        {K : Set (E d)} (hK : MeasurableSet K)
        (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
        (k : E d → ι)
        (hk : ∀ᵐ x ∂uniformMeasure K, ∀ j,
          ⟪x, y j⟫ + c j ≤ ⟪x, y (k x)⟫ + c (k x)) (i : ι) :
        (uniformMeasure K).real {x | k x = i} =
          (uniformMeasure K).real (closedCell K y c i) :=
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

22. theorem OAI.Problem358.CellGeometry.exists_joint_measurable_selector_closedCell_masses line 286

    Source documentation

    A single globally measurable selector works for all parameters. Its masses agree with closed-cell masses at every parameter with distinct slopes, so no injectivity at endpoint parameters or outside the time interval is imposed.

    theorem exists_joint_measurable_selector_closedCell_masses
        {P : Type*} [MeasurableSpace P] [MeasurableSpace ι]
        [Fintype ι] [Nonempty ι]
        {K : Set (E d)} (hK : MeasurableSet K)
        (y : P → ι → E d) (c : P → ι → ℝ)
        (hy : ∀ i, Measurable (fun p => y p i))
        (hc : ∀ i, Measurable (fun p => c p i)) :
        ∃ k : P × E d → ι, Measurable k ∧
          (∀ p x j, ⟪x, y p j⟫ + c p j ≤
            ⟪x, y p (k (p, x))⟫ + c p (k (p, x))) ∧
          ∀ p, Function.Injective (y p) → ∀ i,
            (uniformMeasure K).real {x | k (p, x) = i} =
    …

23. theorem OAI.Problem358.CellGeometry.exists_joint_measurable_selector_prescribed_masses line 312

    Source documentation

    Prescribed closed-cell masses on a chosen set of parameters are realized by one jointly measurable selector, even when sites collide elsewhere.

    theorem exists_joint_measurable_selector_prescribed_masses
        {P : Type*} [MeasurableSpace P] [MeasurableSpace ι]
        [Fintype ι] [Nonempty ι]
        {K : Set (E d)} (hK : MeasurableSet K)
        (y : P → ι → E d) (c m : P → ι → ℝ) (s : Set P)
        (hy : ∀ i, Measurable (fun p => y p i))
        (hc : ∀ i, Measurable (fun p => c p i))
        (hinj : ∀ p ∈ s, Function.Injective (y p))
        (hm : ∀ p ∈ s, ∀ i,
          (uniformMeasure K).real (closedCell K (y p) (c p) i) = m p i) :
        ∃ k : P × E d → ι, Measurable k ∧
          (∀ p x j, ⟪x, y p j⟫ + c p j ≤
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell