OAI/Analysis/Brenier/MovingTrace.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem358.MovingCellTrace.cutIndicator line 13

   Source documentation

   The indicator of a nonnegative affine cut.

   def cutIndicator (r : ℝ) : ℝ := (Set.Ici (0 : ℝ)).indicator (fun _ => 1) r

2. lemma OAI.Problem358.MovingCellTrace.continuousAt_cutIndicator line 15
3. lemma OAI.Problem358.MovingCellTrace.tendsto_cut_product line 21

   Source documentation

   A finite family of cuts is stable whenever every limiting score is nonzero.

   lemma tendsto_cut_product {α ι : Type*} {l : Filter α}
       (J : Finset ι) {s : α → ι → ℝ} {b : ι → ℝ}
       (hs : ∀ i ∈ J, Tendsto (fun a => s a i) l (𝓝 (b i)))
       (hb : ∀ i ∈ J, b i ≠ 0) :
       Tendsto (fun a => ∏ i ∈ J, cutIndicator (s a i)) l
         (𝓝 (∏ i ∈ J, cutIndicator (b i))) := by
   …

   Mentions: OAI.Problem358.MovingCellTrace.cutIndicator

4. lemma OAI.Problem358.MovingCellTrace.tendsto_remainder_trace line 32

   Source documentation

   Generic scaled-trace convergence for the unchanged source constraint and all nonselected moving cuts. The selected face is deliberately absent from J.

   lemma tendsto_remainder_trace {α ι X : Type*} [TopologicalSpace X]
       {l : Filter α} (J : Finset ι) {K : Set X} {w : X → ℝ}
       {x : α → X} {z : X} {s : α → ι → ℝ} {b : ι → ℝ}
       (hx : Tendsto x l (𝓝 z)) (hz : z ∉ frontier K)
       (hw : ContinuousOn w (interior K))
       (hs : ∀ i ∈ J, Tendsto (fun a => s a i) l (𝓝 (b i)))
       (hb : ∀ i ∈ J, b i ≠ 0) :
       Tendsto (fun a => K.indicator w (x a) * ∏ i ∈ J, cutIndicator (s a i)) l
         (𝓝 (K.indicator w z * ∏ i ∈ J, cutIndicator (b i))) := by
   …

   Mentions: OAI.Problem358.MovingCellTrace.cutIndicator

5. lemma OAI.Problem358.MovingCellTrace.tendsto_affine_remainder_trace line 48

   Source documentation

   Affine-score specialization. This permits all sites and intercepts, and the rescaled observation point, to move simultaneously.

   lemma tendsto_affine_remainder_trace {α ι : Type*} {l : Filter α}
       (J : Finset ι) (i : ι) {K : Set F} {w : F → ℝ}
       {x : α → F} {z : F} {y : α → ι → F} {y₀ : ι → F}
       {c : α → ι → ℝ} {c₀ : ι → ℝ}
       (hx : Tendsto x l (𝓝 z)) (hz : z ∉ frontier K)
       (hw : ContinuousOn w (interior K))
       (hy : ∀ k, Tendsto (fun a => y a k) l (𝓝 (y₀ k)))
       (hc : ∀ k, Tendsto (fun a => c a k) l (𝓝 (c₀ k)))
       (hneq : ∀ k ∈ J, ⟪z, y₀ i - y₀ k⟫ + c₀ i - c₀ k ≠ 0) :
       Tendsto (fun a => K.indicator w (x a) * ∏ k ∈ J,
         cutIndicator (⟪x a, y a i - y a k⟫ + c a i - c a k)) l
         (𝓝 (K.indicator w z * ∏ k ∈ J,
   …

   Mentions: OAI.Problem358.MovingCellTrace.cutIndicator

6. lemma OAI.Problem358.MovingCellTrace.tendsto_scaled_affine_remainder_trace line 66

   Source documentation

   The two-sided scaled path required by moving-halfspace differentiation.

   lemma tendsto_scaled_affine_remainder_trace {ι : Type*}
       (J : Finset ι) (i : ι) (y v : ι → F) (c r : ι → ℝ)
       {K : Set F} {w : F → ℝ} {z : F} (n : F) (u : ℝ)
       (hz : z ∉ frontier K) (hw : ContinuousOn w (interior K))
       (hneq : ∀ k ∈ J, ⟪z, y i - y k⟫ + c i - c k ≠ 0) :
       Tendsto (fun h : ℝ => K.indicator w (z + h • (u • n)) * ∏ k ∈ J,
         cutIndicator (⟪z + h • (u • n), (y i + h • v i) - (y k + h • v k)⟫ +
           (c i + h * r i) - (c k + h * r k))) (𝓝 0)
         (𝓝 (K.indicator w z * ∏ k ∈ J,
           cutIndicator (⟪z, y i - y k⟫ + c i - c k))) := by
   …

   Mentions: OAI.Problem358.MovingCellTrace.cutIndicator

7. lemma OAI.Problem358.MovingCellTrace.measurable_cutIndicator line 97
8. lemma OAI.Problem358.MovingCellTrace.norm_cutIndicator_le_one line 100
9. lemma OAI.Problem358.MovingCellTrace.norm_cut_product_le_one line 103
10. lemma OAI.Problem358.MovingCellTrace.measurable_cut_product line 112
11. lemma OAI.Problem358.MovingCellTrace.measurable_remainder line 117
12. lemma OAI.Problem358.MovingCellTrace.norm_remainder_le line 125

    Source documentation

    Removing finitely many halfspace constraints never enlarges the absolute weight.

    lemma norm_remainder_le {ι X : Type*} (J : Finset ι) (K : Set X)
        (w : X → ℝ) (s : X → ι → ℝ) (x : X) :
        ‖K.indicator w x * ∏ i ∈ J, cutIndicator (s x i)‖ ≤ ‖K.indicator w x‖ := by
    …

    Mentions: OAI.Problem358.MovingCellTrace.cutIndicator

13. lemma OAI.Problem358.MovingCellTrace.integrable_remainder line 132
14. lemma OAI.Problem358.MovingCellTrace.integrable_remainder_comp_measurePreserving line 143

    Source documentation

    Ambient integrability transfers to any measure-preserving product chart.

    lemma integrable_remainder_comp_measurePreserving
        {ι X V : Type*} [MeasurableSpace X] [MeasurableSpace V]
        {μ : Measure X} {ν : Measure V} {chart : X → V}
        (hchart : MeasurePreserving chart μ ν)
        (J : Finset ι) {K : Set V} (hK : MeasurableSet K)
        {w : V → ℝ} (hw : IntegrableOn w K ν) {s : V → ι → ℝ}
        (hs : ∀ i ∈ J, Measurable (fun x => s x i)) :
        Integrable (fun p => K.indicator w (chart p) * ∏ i ∈ J,
          cutIndicator (s (chart p) i)) μ := by
    …

    Mentions: OAI.Problem358.MovingCellTrace.cutIndicator

15. lemma OAI.Problem358.MovingCellTrace.norm_remainder_chart_le line 157

    Source documentation

    The transverse support of every cut remainder is inside the projection of the fixed compact source. No bound on the normal coordinate is needed.

    lemma norm_remainder_chart_le {ι X V : Type*}
        (J : Finset ι) (K : Set V) (P : V → X) (chart : X × ℝ → V)
        (hP : ∀ z t, P (chart (z, t)) = z)
        (w : V → ℝ) (s : V → ι → ℝ) {C : ℝ} (hC : 0 ≤ C)
        (hw : ∀ x ∈ K, ‖w x‖ ≤ C) (z : X) (t : ℝ) :
        ‖K.indicator w (chart (z, t)) * ∏ i ∈ J,
          cutIndicator (s (chart (z, t)) i)‖ ≤ (P '' K).indicator (fun _ => C) z := by
    …

    Mentions: OAI.Problem358.MovingCellTrace.cutIndicator

16. lemma OAI.Problem358.MovingCellTrace.integrable_compact_projection_bound line 175

    Source documentation

    Any continuous speed envelope is integrable against a compact transverse support bound. This is the domination premise in the moving-face kernel.

    lemma integrable_compact_projection_bound
        {X V : Type*} [TopologicalSpace X] [MeasurableSpace X]
        [OpensMeasurableSpace X] [T2Space X] [TopologicalSpace V]
        {μ : Measure X} [IsFiniteMeasureOnCompacts μ]
        {K : Set V} (hK : IsCompact K) {P : V → X} (hP : Continuous P)
        {A : X → ℝ} (hA : Continuous A) (C : ℝ) :
        Integrable (fun z => A z * (P '' K).indicator (fun _ => C) z) μ := by
    …

17. theorem OAI.Problem358.MovingCellTrace.exists_compact_projection_domination line 192

    Source documentation

    Compactness discharges a uniform transverse dominating function for every configuration of additional halfspace cuts, at once.

    theorem exists_compact_projection_domination
        {ι Θ X V : Type*} [TopologicalSpace X] [MeasurableSpace X]
        [OpensMeasurableSpace X] [T2Space X] [TopologicalSpace V]
        {μ : Measure X} [IsFiniteMeasureOnCompacts μ]
        (J : Finset ι) {K : Set V} (hK : IsCompact K)
        {P : V → X} (hP : Continuous P) (chart : X × ℝ → V)
        (hchart : ∀ z t, P (chart (z, t)) = z)
        {w : V → ℝ} (hw : ContinuousOn w K)
        (s : Θ → V → ι → ℝ) {A : X → ℝ} (hA : Continuous A) :
        ∃ B : X → ℝ, (∀ z, 0 ≤ B z) ∧ Integrable (fun z => A z * B z) μ ∧
          ∀ a z t, ‖K.indicator w (chart (z, t)) * ∏ i ∈ J,
            cutIndicator (s a (chart (z, t)) i)‖ ≤ B z := by
    …

    Mentions: OAI.Problem358.MovingCellTrace.cutIndicator

18. theorem OAI.Problem358.MovingCellTrace.tendsto_integral_remainder_of_compact_projection line 220

    Source documentation

    Continuity of finite-cut face integrals in a fixed transverse projection. All integrability and domination are consequences of the compact source and continuous test weight. The varying charts need not be measure preserving: the measure here stays on the fixed reference plane.

    theorem tendsto_integral_remainder_of_compact_projection
        {ι α X V : Type*} {l : Filter α} [l.IsCountablyGenerated]
        [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [T2Space X]
        [TopologicalSpace V] [MeasurableSpace V] [OpensMeasurableSpace V] [T2Space V]
        {μ : Measure X} [IsFiniteMeasureOnCompacts μ]
        (J : Finset ι) {K : Set V} (hK : IsCompact K)
        {P : V → X} (hP : Continuous P)
        {chart : α → X → V} {base : X → V}
        (hproject : ∀ q x, P (chart q x) = x)
        (hchartmeas : ∀ q, Measurable (chart q))
        (hchartlim : ∀ᵐ x ∂μ, Tendsto (fun q => chart q x) l (𝓝 (base x)))
        {w : V → ℝ} (hwmeas : Measurable w) (hwcont : ContinuousOn w K)
    …