OAI/Analysis/Brenier/Interfaces.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.interior_affine_preimage_eq line 17

   Source documentation

   If an affine slice meets the interior of a convex set, its relative interior contains no new boundary points of the ambient convex set.

   theorem interior_affine_preimage_eq (f : U →ᵃ[ℝ] V) (hf : Continuous f)
       {K : Set V} (hK : Convex ℝ K) (hmeet : (f ⁻¹' interior K).Nonempty) :
       interior (f ⁻¹' K) = f ⁻¹' interior K := by
   …

2. theorem OAI.Problem358.frontier_affine_preimage_eq line 35

   Source documentation

   Boundary commutes with an affine slice through the interior of a closed convex set.

   theorem frontier_affine_preimage_eq (f : U →ᵃ[ℝ] V) (hf : Continuous f)
       {K : Set V} (hclosed : IsClosed K) (hK : Convex ℝ K)
       (hmeet : (f ⁻¹' interior K).Nonempty) :
       frontier (f ⁻¹' K) = f ⁻¹' frontier K := by
   …

3. theorem OAI.Problem358.haar_affine_preimage_frontier_null line 44

   Source documentation

   The ambient boundary cuts an interior-crossing affine slice in a Haar-null set. This applies to the hyperplane and lower-dimensional fibers in cell differentiation.

   theorem haar_affine_preimage_frontier_null [FiniteDimensional ℝ U]
       [MeasurableSpace U] [BorelSpace U] (μ : Measure U) [IsAddHaarMeasure μ]
       (f : U →ᵃ[ℝ] V) {K : Set V} (hclosed : IsClosed K) (hK : Convex ℝ K)
       (hmeet : (f ⁻¹' interior K).Nonempty) : μ (f ⁻¹' frontier K) = 0 := by
   …

4. theorem OAI.Problem358.ae_continuousAt_indicator_on_affine_slice line 53

   Source documentation

   Continuous integrands restricted to a convex body are continuous almost everywhere along an affine slice crossing its interior.

   theorem ae_continuousAt_indicator_on_affine_slice [FiniteDimensional ℝ U]
       [MeasurableSpace U] [BorelSpace U] (μ : Measure U) [IsAddHaarMeasure μ]
       (f : U →ᵃ[ℝ] V) {K : Set V} (hclosed : IsClosed K) (hK : Convex ℝ K)
       (hmeet : (f ⁻¹' interior K).Nonempty)
       {W : Type*} [TopologicalSpace W] [Zero W] {g : V → W}
       (hg : ContinuousOn g (interior K)) :
       ∀ᵐ x ∂μ, ContinuousAt (K.indicator g) (f x) := by
   …

5. theorem OAI.Problem358.ae_tendsto_indicator_on_affine_slice line 68

   Source documentation

   Moving-slice indicators converge almost everywhere before invoking dominated convergence; no differentiability in the transverse parameter is required.

   theorem ae_tendsto_indicator_on_affine_slice [FiniteDimensional ℝ U]
       [MeasurableSpace U] [BorelSpace U] (μ : Measure U) [IsAddHaarMeasure μ]
       (f : U →ᵃ[ℝ] V) {K : Set V} (hclosed : IsClosed K) (hK : Convex ℝ K)
       (hmeet : (f ⁻¹' interior K).Nonempty)
       {W : Type*} [TopologicalSpace W] [Zero W] {g : V → W}
       (hg : ContinuousOn g (interior K))
       {A : Type*} {l : Filter A} {F : A → U → V}
       (hF : ∀ᵐ x ∂μ, Filter.Tendsto (fun a => F a x) l (𝓝 (f x))) :
       ∀ᵐ x ∂μ, Filter.Tendsto (fun a => K.indicator g (F a x)) l
         (𝓝 (K.indicator g (f x))) := by
   …

6. theorem OAI.Problem358.CellGeometry.ae_regular_interface line 97

   Source documentation

   Positive-mass affine cells have regular interfaces: the source boundary and all third-branch ties are negligible for surface Haar measure.

   theorem ae_regular_interface {ρ : Measure (E d)} (hρ : ρ ≪ volume)
       {K : Set (E d)} (hclosed : IsClosed K) (hconv : Convex ℝ K)
       (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
       (hpos : ∀ k, ρ (closedCell K y c k) ≠ 0)
       {i j : ι} (hij : i ≠ j) {z : E d} (hz : z ∈ interior K)
       (htie : inner ℝ z (y i) + c i = inner ℝ z (y j) + c j)
       (μ : Measure ((ℝ ∙ (y i - y j))ᗮ)) [μ.IsAddHaarMeasure] :
       ∀ᵐ w : (ℝ ∙ (y i - y j))ᗮ ∂μ,
         z + (w : E d) ∉ frontier K ∧ ∀ k, k ≠ i → k ≠ j →
         inner ℝ (z + (w : E d)) (y i) + c i ≠
           inner ℝ (z + (w : E d)) (y k) + c k := by
   …

   Mentions: OAI.Problem358.CellGeometry.closedCell

7. theorem OAI.Problem358.CellGeometry.eventually_mem_iff_of_not_mem_frontier line 125

   Source documentation

   Membership in a set is eventually constant under convergence away from its boundary.

   theorem eventually_mem_iff_of_not_mem_frontier {X A : Type*} [TopologicalSpace X]
       {s : Set X} {x : X} (hx : x ∉ frontier s) {l : Filter A} {f : A → X}
       (hf : Tendsto f l (𝓝 x)) : ∀ᶠ a in l, f a ∈ s ↔ x ∈ s := by
   …

8. theorem OAI.Problem358.CellGeometry.eventually_le_iff_of_tendsto_ne line 138

   Source documentation

   A strict limiting inequality has an eventually constant weak-inequality indicator.

   theorem eventually_le_iff_of_tendsto_ne {A : Type*} {l : Filter A}
       {f g : A → ℝ} {a b : ℝ} (hf : Tendsto f l (𝓝 a))
       (hg : Tendsto g l (𝓝 b)) (hne : a ≠ b) :
       ∀ᶠ t in l, f t ≤ g t ↔ a ≤ b := by
   …

9. theorem OAI.Problem358.CellGeometry.ae_eventually_stable_interface line 151

   Source documentation

   The unchanged cell factors in a moving-interface argument are eventually constant at surface-almost every point. Both source points and affine branches may vary along an arbitrary filter.

   theorem ae_eventually_stable_interface {ρ : Measure (E d)} (hρ : ρ ≪ volume)
       {K : Set (E d)} (hclosed : IsClosed K) (hconv : Convex ℝ K)
       (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
       (hpos : ∀ k, ρ (closedCell K y c k) ≠ 0)
       {i j : ι} (hij : i ≠ j) {z : E d} (hz : z ∈ interior K)
       (htie : inner ℝ z (y i) + c i = inner ℝ z (y j) + c j)
       (μ : Measure ((ℝ ∙ (y i - y j))ᗮ)) [μ.IsAddHaarMeasure]
       {A : Type*} {l : Filter A}
       {F : A → ((ℝ ∙ (y i - y j))ᗮ) → E d}
       {y' : A → ι → E d} {c' : A → ι → ℝ}
       (hy' : ∀ k, Tendsto (fun a => y' a k) l (𝓝 (y k)))
       (hc' : ∀ k, Tendsto (fun a => c' a k) l (𝓝 (c k)))
   …

   Mentions: OAI.Problem358.CellGeometry.closedCell

10. theorem OAI.Problem358.CellGeometry.ae_regular_interface_of_tie line 200

    Source documentation

    The regular-interface theorem for an arbitrary point on the equality plane. Positive cell masses supply an interior crossing, so the chosen affine-chart base need not itself belong to the convex source.

    theorem ae_regular_interface_of_tie
        {d : ℕ} {ι : Type*} [Fintype ι]
        {ρ : Measure (E d)} (hρ : ρ ≪ volume)
        {K : Set (E d)} (hclosed : IsClosed K) (hconv : Convex ℝ K)
        (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
        (hpos : ∀ k, ρ (closedCell K y c k) ≠ 0)
        {i j : ι} (hij : i ≠ j) {z : E d}
        (htie : inner ℝ z (y i) + c i = inner ℝ z (y j) + c j)
        (μ : Measure ((ℝ ∙ (y i - y j))ᗮ)) [μ.IsAddHaarMeasure] :
        ∀ᵐ w : (ℝ ∙ (y i - y j))ᗮ ∂μ,
          z + (w : E d) ∉ frontier K ∧ ∀ k, k ≠ i → k ≠ j →
          inner ℝ (z + (w : E d)) (y i) + c i ≠
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

11. theorem OAI.Problem358.MovingCellTrace.ae_tendsto_interface_remainder line 252

    Source documentation

    The actual surface-almost-everywhere trace needed by moving-cell differentiation. Regularity is derived from positive cells, rather than assumed. The varying cut normals are independent, so this also permits the mixed current/base cuts in the finite-product telescoping identity.

    theorem ae_tendsto_interface_remainder
        {d : ℕ} {ι α U : Type*} [Fintype ι] {l : Filter α}
        {ρ : Measure (E d)} (hρ : ρ ≪ volume)
        {K : Set (E d)} (hclosed : IsClosed K) (hconv : Convex ℝ K)
        (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
        (hpos : ∀ k, ρ (CellGeometry.closedCell K y c k) ≠ 0)
        {i j : ι} (hij : i ≠ j) {z : E d} (hz : z ∈ interior K)
        (htie : ⟪z, y i⟫ + c i = ⟪z, y j⟫ + c j)
        (μ : Measure ((ℝ ∙ (y i - y j))ᗮ)) [μ.IsAddHaarMeasure]
        (J : Finset ι) (hJ : ∀ k ∈ J, k ≠ i ∧ k ≠ j)
        {w : E d → ℝ} (hw : ContinuousOn w (interior K))
        {F : α → U → ((ℝ ∙ (y i - y j))ᗮ) → E d}
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell