OAI/Analysis/Brenier/FaceContinuity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.MovingCellTrace.tendsto_positive_cell_face_integral line 15

   Source documentation

   Weighted face coefficients vary continuously for positive affine cells, expressed in any nearby-plane chart preserving a fixed transverse projection. The compact source supplies domination; positivity supplies all surface nullity.

   theorem tendsto_positive_cell_face_integral
       {d : ℕ} {ι α : Type*} [Fintype ι] {l : Filter α} [l.IsCountablyGenerated]
       {ρ : Measure (E d)} (hρ : ρ ≪ volume)
       {K : Set (E d)} (hK : IsCompact 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)
       {P : E d → (ℝ ∙ (y i - y j))ᗮ} (hP : Continuous P)
       {chart : α → ((ℝ ∙ (y i - y j))ᗮ) → E d}
   …

   Mentions: OAI.Problem358.CellGeometry.closedCell

2. def OAI.Problem358.AffinePlaneGraph.unitNormal line 71

   Source documentation

   Unit transverse vector of a nonzero reference normal.

   def unitNormal (n : E d) : E d := ‖n‖⁻¹ • n

3. lemma OAI.Problem358.AffinePlaneGraph.inner_unitNormal line 73
4. def OAI.Problem358.AffinePlaneGraph.tangentProjection line 79

   Source documentation

   Fixed tangential coordinates relative to a chosen point of the reference plane.

   def tangentProjection (n z : E d) : E d → (ℝ ∙ n)ᗮ :=
   …

5. lemma OAI.Problem358.AffinePlaneGraph.continuous_tangentProjection line 82
6. lemma OAI.Problem358.AffinePlaneGraph.tangentProjection_add line 86
7. def OAI.Problem358.AffinePlaneGraph.interfaceGraph line 98

   Source documentation

   Reference-normal graph coordinates for a varying selected interface.

   def interfaceGraph (n₀ z : E d) (a : ι → E d) (b : ι → ℝ) (i j : ι) :
       (ℝ ∙ n₀)ᗮ → E d :=
   …

8. def OAI.Problem358.AffinePlaneGraph.faceCoefficient line 104

   Source documentation

   A transverse face coefficient; the fixed-plane measure and transverse normal factor together are the disintegration coefficient in cell derivatives.

   def faceCoefficient (K : Set (E d)) (n₀ z : E d) (J : Finset ι)
       (i j : ι) (w : E d → ℝ) (p : (ι → E d) × (ι → ℝ)) : ℝ :=
   …

9. theorem OAI.Problem358.AffinePlaneGraph.tendsto_faceCoefficient line 116

   Source documentation

   Continuity of actual weighted positive-cell face coefficients, with the nearby charts, compact domination, and surface nullity all furnished internally. Only the reference configuration needs positive cells.

   theorem tendsto_faceCoefficient
       {α : Type*} {l : Filter α} [l.IsCountablyGenerated]
       {ρ : Measure (E d)} (hρ : ρ ≪ volume)
       {K : Set (E d)} (hK : IsCompact 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)
       (J : Finset ι) (hJ : ∀ k ∈ J, k ≠ i ∧ k ≠ j)
       {w : E d → ℝ} (hw : Continuous w)
       {a : α → ι → E d} {b : α → ι → ℝ}
       (ha : ∀ k, Tendsto (fun q => a q k) l (𝓝 (y k)))
   …

   Mentions: OAI.Problem358.CellGeometry.closedCell

10. theorem OAI.Problem358.AffinePlaneGraph.continuousAt_faceCoefficient line 169

    Source documentation

    Local continuity on the full joint site/intercept parameter space.

    theorem continuousAt_faceCoefficient
        {ρ : Measure (E d)} (hρ : ρ ≪ volume)
        {K : Set (E d)} (hK : IsCompact 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)
        (J : Finset ι) (hJ : ∀ k ∈ J, k ≠ i ∧ k ≠ j)
        {w : E d → ℝ} (hw : Continuous w) :
        ContinuousAt (faceCoefficient K (y i - y j) z J i j w) (y, c) := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.AffinePlaneGraph.faceCoefficient

11. theorem OAI.Problem358.MovingCellTrace.tendsto_positive_cell_face_integral_of_tie line 196

    Source documentation

    Weighted face coefficients vary continuously for positive affine cells, expressed in any nearby-plane chart preserving a fixed transverse projection. The compact source supplies domination; positivity supplies all surface nullity.

    theorem tendsto_positive_cell_face_integral_of_tie
        {d : ℕ} {ι α : Type*} [Fintype ι] {l : Filter α} [l.IsCountablyGenerated]
        {ρ : Measure (E d)} (hρ : ρ ≪ volume)
        {K : Set (E d)} (hK : IsCompact 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}
        (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)
        {P : E d → (ℝ ∙ (y i - y j))ᗮ} (hP : Continuous P)
        {chart : α → ((ℝ ∙ (y i - y j))ᗮ) → E d}
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

12. theorem OAI.Problem358.AffinePlaneGraph.tendsto_faceCoefficient_of_tie line 247

    Source documentation

    Continuity of actual weighted positive-cell face coefficients, with the nearby charts, compact domination, and surface nullity all furnished internally. Only the reference configuration needs positive cells.

    theorem tendsto_faceCoefficient_of_tie
        {α : Type*} {l : Filter α} [l.IsCountablyGenerated]
        {ρ : Measure (E d)} (hρ : ρ ≪ volume)
        {K : Set (E d)} (hK : IsCompact 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}
        (htie : ⟪z, y i⟫ + c i = ⟪z, y j⟫ + c j)
        (J : Finset ι) (hJ : ∀ k ∈ J, k ≠ i ∧ k ≠ j)
        {w : E d → ℝ} (hw : Continuous w)
        {a : α → ι → E d} {b : α → ι → ℝ}
        (ha : ∀ k, Tendsto (fun q => a q k) l (𝓝 (y k)))
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

13. theorem OAI.Problem358.AffinePlaneGraph.continuousAt_faceCoefficient_of_tie line 300

    Source documentation

    Local continuity on the full joint site/intercept parameter space.

    theorem continuousAt_faceCoefficient_of_tie
        {ρ : Measure (E d)} (hρ : ρ ≪ volume)
        {K : Set (E d)} (hK : IsCompact 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}
        (htie : ⟪z, y i⟫ + c i = ⟪z, y j⟫ + c j)
        (J : Finset ι) (hJ : ∀ k ∈ J, k ≠ i ∧ k ≠ j)
        {w : E d → ℝ} (hw : Continuous w) :
        ContinuousAt (faceCoefficient K (y i - y j) z J i j w) (y, c) := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.AffinePlaneGraph.faceCoefficient

14. def OAI.Problem358.AffinePlaneGraph.intrinsicCutCoefficient line 329

    Source documentation

    The normalized intrinsic integral over an interface with additional affine cuts. Unlike the local faceCoefficient, this definition uses no reference normal or basepoint.

    def intrinsicCutCoefficient (K : Set (E d)) (J : Finset ι) (i j : ι)
        (w : E d → ℝ) (p : (ι → E d) × (ι → ℝ)) : ℝ :=
    …

15. theorem OAI.Problem358.AffinePlaneGraph.faceCoefficient_eq_intrinsicCutCoefficient line 338

    Source documentation

    The fixed transverse coefficient equals the intrinsic coefficient throughout the neighborhood where the transverse orientation stays positive.

    theorem faceCoefficient_eq_intrinsicCutCoefficient
        {K : Set (E d)} (hK : MeasurableSet K) (n₀ z : E d) (hn₀ : n₀ ≠ 0)
        (J : Finset ι) (i j : ι) (w : E d → ℝ) (hw : Measurable w)
        (p : (ι → E d) × (ι → ℝ))
        (htrans : 0 < ⟪p.1 i - p.1 j, unitNormal n₀⟫) :
        faceCoefficient K n₀ z J i j w p = intrinsicCutCoefficient K J i j w p := by
    …

    Mentions: OAI.Problem358.AffinePlaneGraph.unitNormal, OAI.Problem358.AffinePlaneGraph.faceCoefficient, OAI.Problem358.AffinePlaneGraph.intrinsicCutCoefficient

16. theorem OAI.Problem358.AffinePlaneGraph.continuousAt_intrinsicCutCoefficient line 376

    Source documentation

    Actual intrinsic face coefficients are continuous in all sites and intercepts at each positive-cell configuration. No choice of a moving frame, Jacobian, exceptional set, or local derivative field is left as a hypothesis.

    theorem continuousAt_intrinsicCutCoefficient [Fintype ι]
        {ρ : Measure (E d)} (hρ : ρ ≪ volume)
        {K : Set (E d)} (hK : IsCompact 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)
        (J : Finset ι) (hJ : ∀ k ∈ J, k ≠ i ∧ k ≠ j)
        {w : E d → ℝ} (hw : Continuous w) :
        ContinuousAt (intrinsicCutCoefficient K J i j w) (y, c) := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.AffinePlaneGraph.intrinsicCutCoefficient