OAI/Analysis/Brenier/CellContinuity.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem358.scoreCell line 13

   Source documentation

   The closed cell of an affine score, before restriction to the source set.

   def scoreCell {d : ℕ} {ι : Type*} (y : ι → E d) (c : ι → ℝ) (i : ι) : Set (E d) :=
   …

2. theorem OAI.Problem358.measurableSet_scoreCell line 16
3. theorem OAI.Problem358.eventually_le_iff_of_tendsto_ne line 24

   Source documentation

   A strict limiting comparison has an eventually constant truth value.

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

4. theorem OAI.Problem358.eventually_mem_scoreCell_iff line 35

   Source documentation

   Away from limiting ties, membership in a finite affine cell stabilizes.

   theorem eventually_mem_scoreCell_iff {d : ℕ} {ι β : Type*} [Finite ι]
       {l : Filter β} {ys : β → ι → E d} {cs : β → ι → ℝ}
       {y : ι → E d} {c : ι → ℝ} (i : ι) (x : E d)
       (hy : ∀ j, Tendsto (fun n => ys n j) l (𝓝 (y j)))
       (hc : ∀ j, Tendsto (fun n => cs n j) l (𝓝 (c j)))
       (htie : ∀ j, j ≠ i → inner ℝ (y j) x + c j ≠ inner ℝ (y i) x + c i) :
       ∀ᶠ n in l, x ∈ scoreCell (ys n) (cs n) i ↔ x ∈ scoreCell y c i := by
   …

   Mentions: OAI.Problem358.scoreCell

5. theorem OAI.Problem358.ae_eventually_mem_scoreCell_iff line 56

   Source documentation

   Distinct limiting slopes make affine-cell membership stabilize almost everywhere.

   theorem ae_eventually_mem_scoreCell_iff {d : ℕ} {ι β : Type*} [Finite ι]
       (K : Set (E d)) {l : Filter β} {ys : β → ι → E d} {cs : β → ι → ℝ}
       {y : ι → E d} {c : ι → ℝ} (i : ι) (hinj : Function.Injective y)
       (hy : ∀ j, Tendsto (fun n => ys n j) l (𝓝 (y j)))
       (hc : ∀ j, Tendsto (fun n => cs n j) l (𝓝 (c j))) :
       ∀ᵐ x ∂uniformMeasure K, ∀ᶠ n in l,
         x ∈ scoreCell (ys n) (cs n) i ↔ x ∈ scoreCell y c i := by
   …

   Mentions: OAI.Problem358.scoreCell

6. theorem OAI.Problem358.tendsto_uniformMeasure_scoreCell line 70

   Source documentation

   Cell masses converge under convergence of sites and intercepts, provided only that the limiting sites are distinct and the uniform source is finite.

   theorem tendsto_uniformMeasure_scoreCell {d : ℕ} {ι β : Type*} [Finite ι]
       (K : Set (E d))
       {l : Filter β} [l.IsCountablyGenerated]
       {ys : β → ι → E d} {cs : β → ι → ℝ} {y : ι → E d} {c : ι → ℝ}
       (i : ι) (hinj : Function.Injective y)
       (hy : ∀ j, Tendsto (fun n => ys n j) l (𝓝 (y j)))
       (hc : ∀ j, Tendsto (fun n => cs n j) l (𝓝 (c j))) :
       Tendsto (fun n => uniformMeasure K (scoreCell (ys n) (cs n) i)) l
         (𝓝 (uniformMeasure K (scoreCell y c i))) := by
   …

   Mentions: OAI.Problem358.scoreCell

7. theorem OAI.Problem358.continuousAt_uniformMeasure_scoreCell line 85

   Source documentation

   Joint continuity in all affine coefficients at configurations with distinct sites.

   theorem continuousAt_uniformMeasure_scoreCell {d : ℕ} {ι : Type*} [Finite ι]
       (K : Set (E d))
       (y : ι → E d) (c : ι → ℝ) (i : ι) (hinj : Function.Injective y) :
       ContinuousAt (fun p : (ι → E d) × (ι → ℝ) =>
         uniformMeasure K (scoreCell p.1 p.2 i)) (y, c) := by
   …

   Mentions: OAI.Problem358.scoreCell

8. theorem OAI.Problem358.tendsto_setIntegral_of_ae_eventually_mem line 98

   Source documentation

   Dominated convergence for an integrable function over varying measurable sets whose membership stabilizes almost everywhere.

   theorem tendsto_setIntegral_of_ae_eventually_mem
       {X V β : Type*} [MeasurableSpace X] [NormedAddCommGroup V] [NormedSpace ℝ V]
       {μ : Measure X} {l : Filter β} [l.IsCountablyGenerated]
       {sets : β → Set X} {s : Set X} (hsets : ∀ n, MeasurableSet (sets n))
       (hs : MeasurableSet s) {f : X → V} (hf : Integrable f μ)
       (hmem : ∀ᵐ x ∂μ, ∀ᶠ n in l, x ∈ sets n ↔ x ∈ s) :
       Tendsto (fun n => ∫ x in sets n, f x ∂μ) l (𝓝 (∫ x in s, f x ∂μ)) := by
   …

9. theorem OAI.Problem358.tendsto_setIntegral_scoreCell line 122

   Source documentation

   Integrals over affine cells, including their first moments, converge jointly in all coefficients whenever the limiting slopes are distinct.

   theorem tendsto_setIntegral_scoreCell {d : ℕ} {ι β V : Type*} [Finite ι]
       [NormedAddCommGroup V] [NormedSpace ℝ V]
       (K : Set (E d)) {l : Filter β} [l.IsCountablyGenerated]
       {ys : β → ι → E d} {cs : β → ι → ℝ} {y : ι → E d} {c : ι → ℝ}
       (i : ι) (hinj : Function.Injective y)
       (hy : ∀ j, Tendsto (fun n => ys n j) l (𝓝 (y j)))
       (hc : ∀ j, Tendsto (fun n => cs n j) l (𝓝 (c j)))
       {f : E d → V} (hf : Integrable f (uniformMeasure K)) :
       Tendsto (fun n => ∫ x in scoreCell (ys n) (cs n) i, f x ∂uniformMeasure K) l
         (𝓝 (∫ x in scoreCell y c i, f x ∂uniformMeasure K)) :=
   …

   Mentions: OAI.Problem358.scoreCell

10. theorem OAI.Problem358.continuousAt_setIntegral_scoreCell line 137

    Source documentation

    Joint continuity of any integrable moment of a finite affine cell.

    theorem continuousAt_setIntegral_scoreCell {d : ℕ} {ι V : Type*} [Finite ι]
        [NormedAddCommGroup V] [NormedSpace ℝ V]
        (K : Set (E d)) (y : ι → E d) (c : ι → ℝ) (i : ι)
        (hinj : Function.Injective y) {f : E d → V} (hf : Integrable f (uniformMeasure K)) :
        ContinuousAt (fun p : (ι → E d) × (ι → ℝ) =>
          ∫ x in scoreCell p.1 p.2 i, f x ∂uniformMeasure K) (y, c) := by
    …

    Mentions: OAI.Problem358.scoreCell

11. theorem OAI.Problem358.eventually_injective_sites line 151

    Source documentation

    Distinctness of a finite family of sites persists locally.

    theorem eventually_injective_sites {d : ℕ} {ι : Type*} [Finite ι]
        (y : ι → E d) (c : ι → ℝ) (hinj : Function.Injective y) :
        ∀ᶠ p : (ι → E d) × (ι → ℝ) in 𝓝 (y, c), Function.Injective p.1 := by
    …

12. theorem OAI.Problem358.isOpen_distinct_positive_scoreCell line 171

    Source documentation

    The configurations on which the finite-cell differential calculus is used (distinct sites and strictly positive cell masses) form an open set.

    theorem isOpen_distinct_positive_scoreCell {d : ℕ} {ι : Type*} [Finite ι]
        (K : Set (E d)) :
        IsOpen {p : (ι → E d) × (ι → ℝ) |
          Function.Injective p.1 ∧ ∀ i, 0 < uniformMeasure K (scoreCell p.1 p.2 i)} := by
    …

    Mentions: OAI.Problem358.scoreCell

13. theorem OAI.Problem358.CellGeometry.closedCell_eq_inter_scoreCell line 193

    Source documentation

    The geometric closed cell is the score cell restricted to the source body.

    theorem closedCell_eq_inter_scoreCell
        (K : Set (E d)) (y : ι → E d) (c : ι → ℝ) (i : ι) :
        closedCell K y c i = K ∩ scoreCell y c i := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.scoreCell

14. theorem OAI.Problem358.CellGeometry.closedCell_ae_eq_scoreCell line 201

    Source documentation

    The two cell conventions agree almost everywhere for the uniform source.

    theorem closedCell_ae_eq_scoreCell {K : Set (E d)} (hK : MeasurableSet K)
        (y : ι → E d) (c : ι → ℝ) (i : ι) :
        closedCell K y c i =ᵐ[uniformMeasure K] scoreCell y c i := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.scoreCell

15. theorem OAI.Problem358.CellGeometry.restrict_closedCell_eq_scoreCell line 209

    Source documentation

    Restricting the uniform source is independent of the cell convention.

    theorem restrict_closedCell_eq_scoreCell {K : Set (E d)} (hK : MeasurableSet K)
        (y : ι → E d) (c : ι → ℝ) (i : ι) :
        (uniformMeasure K).restrict (closedCell K y c i) =
          (uniformMeasure K).restrict (scoreCell y c i) :=
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.scoreCell

16. theorem OAI.Problem358.CellGeometry.uniformMeasure_closedCell_eq_scoreCell line 216

    Source documentation

    Closed-cell masses are exactly the score-cell masses.

    theorem uniformMeasure_closedCell_eq_scoreCell {K : Set (E d)} (hK : MeasurableSet K)
        (y : ι → E d) (c : ι → ℝ) (i : ι) :
        uniformMeasure K (closedCell K y c i) = uniformMeasure K (scoreCell y c i) :=
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell, OAI.Problem358.scoreCell

17. theorem OAI.Problem358.CellGeometry.continuousAt_uniformMeasure_closedCell line 222

    Source documentation

    Joint continuity of the actual geometric closed-cell mass at distinct sites.

    theorem continuousAt_uniformMeasure_closedCell [Finite ι]
        {K : Set (E d)} (hK : MeasurableSet K)
        (y : ι → E d) (c : ι → ℝ) (i : ι) (hinj : Function.Injective y) :
        ContinuousAt (fun p : (ι → E d) × (ι → ℝ) =>
          uniformMeasure K (closedCell K p.1 p.2 i)) (y, c) := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

18. theorem OAI.Problem358.CellGeometry.continuousAt_real_closedCell line 231

    Source documentation

    Real-valued closed-cell masses are jointly continuous at distinct sites.

    theorem continuousAt_real_closedCell [Finite ι]
        {K : Set (E d)} (hK : MeasurableSet K)
        (y : ι → E d) (c : ι → ℝ) (i : ι) (hinj : Function.Injective y) :
        ContinuousAt (fun p : (ι → E d) × (ι → ℝ) =>
          (uniformMeasure K).real (closedCell K p.1 p.2 i)) (y, c) := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

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

    Source documentation

    Cell integral continuity transfers to the geometric closed-cell convention.

    theorem continuousAt_setIntegral_closedCell [Finite ι]
        {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
        {K : Set (E d)} (hK : MeasurableSet K)
        (y : ι → E d) (c : ι → ℝ) (i : ι) (hinj : Function.Injective y)
        {f : E d → V} (hf : Integrable f (uniformMeasure K)) :
        ContinuousAt (fun p : (ι → E d) × (ι → ℝ) =>
          ∫ x in closedCell K p.1 p.2 i, f x ∂uniformMeasure K) (y, c) := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

20. theorem OAI.Problem358.CellGeometry.continuousAt_firstMoment_closedCell line 255

    Source documentation

    The actual first moment of a closed cell is jointly continuous.

    theorem continuousAt_firstMoment_closedCell [Finite ι]
        {K : Set (E d)} (hK : IsCompact K)
        (y : ι → E d) (c : ι → ℝ) (i : ι) (hinj : Function.Injective y) :
        ContinuousAt (fun p : (ι → E d) × (ι → ℝ) =>
          ∫ x in closedCell K p.1 p.2 i, x ∂uniformMeasure K) (y, c) :=
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

21. theorem OAI.Problem358.CellGeometry.isOpen_distinct_positive_real_closedCell line 265

    Source documentation

    The admissible locus used by geometric cell calculus is open, in the real-mass convention of the normalized implicit-function construction.

    theorem isOpen_distinct_positive_real_closedCell [Finite ι]
        {K : Set (E d)} (hK : MeasurableSet K) :
        IsOpen {p : (ι → E d) × (ι → ℝ) |
          Function.Injective p.1 ∧ ∀ i, 0 < (uniformMeasure K).real (closedCell K p.1 p.2 i)} := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell

22. theorem OAI.Problem358.CellGeometry.eventually_real_closedCell_comparable line 282

    Source documentation

    All positive cell masses simultaneously stay between half and twice their original masses in a neighborhood of a distinct-site configuration.

    theorem eventually_real_closedCell_comparable [Finite ι]
        {K : Set (E d)} (hK : MeasurableSet K)
        (y : ι → E d) (c : ι → ℝ) (hinj : Function.Injective y)
        (hpos : ∀ i, 0 < (uniformMeasure K).real (closedCell K y c i)) :
        ∀ᶠ p : (ι → E d) × (ι → ℝ) in 𝓝 (y, c), ∀ i,
          (uniformMeasure K).real (closedCell K y c i) / 2 <
            (uniformMeasure K).real (closedCell K p.1 p.2 i) ∧
          (uniformMeasure K).real (closedCell K p.1 p.2 i) <
            2 * (uniformMeasure K).real (closedCell K y c i) := by
    …

    Mentions: OAI.Problem358.CellGeometry.closedCell