OAI/Analysis/Brenier/MapLimits.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.tendsto_integral_boundedContinuous_comp_ae line 14

   Source documentation

   Bounded continuous tests commute with almost-everywhere limits of measurable maps on a finite measure space. No uniform bound on the maps themselves is needed.

   theorem tendsto_integral_boundedContinuous_comp_ae
       {X Y : Type*} [MeasurableSpace X] [TopologicalSpace Y]
       [MeasurableSpace Y] [OpensMeasurableSpace Y]
       {ρ : Measure X} [IsFiniteMeasure ρ]
       {Tn : ℕ → X → Y} {T : X → Y}
       (hTn : ∀ n, Measurable (Tn n))
       (hlim : ∀ᵐ x ∂ρ, Tendsto (fun n => Tn n x) atTop (𝓝 (T x)))
       (f : Y →ᵇ ℝ) :
       Tendsto (fun n => ∫ x, f (Tn n x) ∂ρ) atTop
         (𝓝 (∫ x, f (T x) ∂ρ)) := by
   …

2. theorem OAI.Problem358.map_eq_of_ae_tendsto_and_test_tendsto line 35

   Source documentation

   A candidate almost-everywhere limit has the prescribed target law whenever the approximating laws converge against bounded continuous functions.

   theorem map_eq_of_ae_tendsto_and_test_tendsto
       {X Y : Type*} [MeasurableSpace X] [TopologicalSpace Y]
       [MeasurableSpace Y] [BorelSpace Y] [HasOuterApproxClosed Y]
       {ρ : Measure X} [IsFiniteMeasure ρ]
       {ν : Measure Y} [IsFiniteMeasure ν]
       {Tn : ℕ → X → Y} {T : X → Y}
       (hTn : ∀ n, Measurable (Tn n)) (hT : Measurable T)
       (hlim : ∀ᵐ x ∂ρ, Tendsto (fun n => Tn n x) atTop (𝓝 (T x)))
       (htest : ∀ f : Y →ᵇ ℝ,
         Tendsto (fun n => ∫ x, f (Tn n x) ∂ρ) atTop (𝓝 (∫ y, f y ∂ν))) :
       Measure.map T ρ = ν := by
   …

3. theorem OAI.Problem358.ae_mem_of_closed_of_ae_tendsto line 52

   Source documentation

   Closed support constraints survive almost-everywhere limits.

   theorem ae_mem_of_closed_of_ae_tendsto
       {X Y : Type*} [MeasurableSpace X] [TopologicalSpace Y]
       {ρ : Measure X} {Tn : ℕ → X → Y} {T : X → Y} {K : Set Y}
       (hK : IsClosed K) (hmem : ∀ n, ∀ᵐ x ∂ρ, Tn n x ∈ K)
       (hlim : ∀ᵐ x ∂ρ, Tendsto (fun n => Tn n x) atTop (𝓝 (T x))) :
       ∀ᵐ x ∂ρ, T x ∈ K := by
   …

4. theorem OAI.Problem358.map_eq_of_ae_tendsto_quantized line 64

   Source documentation

   The limit of maps to quantized target laws has the original target law. This is the law-identification step in finite-target approximation.

   theorem map_eq_of_ae_tendsto_quantized
       {X Y : Type*} [MeasurableSpace X] [TopologicalSpace Y]
       [MeasurableSpace Y] [BorelSpace Y] [HasOuterApproxClosed Y]
       {ρ : Measure X} [IsFiniteMeasure ρ]
       {ν : Measure Y} [IsFiniteMeasure ν]
       {Tn : ℕ → X → Y} {T : X → Y} {Qn : ℕ → Y → Y}
       (hTn : ∀ n, Measurable (Tn n)) (hT : Measurable T)
       (hQn : ∀ n, Measurable (Qn n))
       (hpush : ∀ n, Measure.map (Tn n) ρ = Measure.map (Qn n) ν)
       (hlim : ∀ᵐ x ∂ρ, Tendsto (fun n => Tn n x) atTop (𝓝 (T x)))
       (hQlim : ∀ᵐ y ∂ν, Tendsto (fun n => Qn n y) atTop (𝓝 y)) :
       Measure.map T ρ = ν := by
   …

5. theorem OAI.Problem358.tendsto_integral_boundedContinuous_comp_of_ae line 86

   Source documentation

   Almost-everywhere convergence gives convergence against bounded continuous tests.

   theorem tendsto_integral_boundedContinuous_comp_of_ae
       {X V : Type*} [MeasurableSpace X] [TopologicalSpace V]
       [MeasurableSpace V] [BorelSpace V]
       {ρ : Measure X} [IsFiniteMeasure ρ]
       {Tn : ℕ → X → V} {T : X → V} (hTn : ∀ n, Measurable (Tn n))
       (hlim : ∀ᵐ x ∂ρ, Tendsto (fun n => Tn n x) atTop (𝓝 (T x)))
       (f : BoundedContinuousFunction V ℝ) :
       Tendsto (fun n => ∫ x, f (Tn n x) ∂ρ) atTop (𝓝 (∫ x, f (T x) ∂ρ)) :=
   …

6. theorem OAI.Problem358.map_eq_of_ae_limits line 97

   Source documentation

   Almost-everywhere limits with convergent approximating laws have the prescribed pushforward.

   theorem map_eq_of_ae_limits
       {X V : Type*} [MeasurableSpace X] [TopologicalSpace V]
       [MeasurableSpace V] [BorelSpace V] [HasOuterApproxClosed V]
       {ρ : Measure X} {μ : Measure V} [IsFiniteMeasure ρ] [IsFiniteMeasure μ]
       {Tn : ℕ → X → V} {T : X → V} {Qn : ℕ → V → V}
       (hTn : ∀ n, Measurable (Tn n)) (hT : Measurable T)
       (hQn : ∀ n, Measurable (Qn n))
       (hTlim : ∀ᵐ x ∂ρ, Tendsto (fun n => Tn n x) atTop (𝓝 (T x)))
       (hQlim : ∀ᵐ y ∂μ, Tendsto (fun n => Qn n y) atTop (𝓝 y))
       (hpush : ∀ n, Measure.map (Tn n) ρ = Measure.map (Qn n) μ) :
       Measure.map T ρ = μ :=
   …

7. theorem OAI.Problem358.exists_measurable_limit_with_property line 123

   Source documentation

   Almost-everywhere existence of a pointwise limit with an arbitrary extra property can be realized by one measurable function. No measurability of the extra property is required.

   theorem exists_measurable_limit_with_property
       {α β : Type*} [MeasurableSpace α] [MetricSpace β]
       [MeasurableSpace β] [BorelSpace β] [Nonempty β]
       {ρ : Measure α} {f : ℕ → α → β} {P : α → β → Prop}
       (hmeas : ∀ n, AEMeasurable (f n) ρ)
       (hex : ∀ᵐ x ∂ρ, ∃ y, Tendsto (fun n => f n x) atTop (𝓝 y) ∧ P x y) :
       ∃ g : α → β, Measurable g ∧ ∀ᵐ x ∂ρ,
         Tendsto (fun n => f n x) atTop (𝓝 (g x)) ∧ P x (g x) := by
   …

8. theorem OAI.Problem358.map_eq_of_mapL2Dist_limit line 162

   Source documentation

   An L² limit has the target law when the approximating laws come from maps converging to identity on that target.

   theorem map_eq_of_mapL2Dist_limit [IsFiniteMeasure ρ] [IsFiniteMeasure ν]
       {T Q : ℕ → E d → E d} {S : E d → E d}
       (hT : ∀ n, Measurable (T n)) (hQ : ∀ n, Measurable (Q n))
       (hS : Measurable S) (hTmem : ∀ n, MemLp (T n) 2 ρ) (hSmem : MemLp S 2 ρ)
       (hTlim : Tendsto (fun n => mapL2Dist ρ (T n) S) atTop (𝓝 0))
       (hQlim : ∀ᵐ y ∂ν, Tendsto (fun n => Q n y) atTop (𝓝 y))
       (hmap : ∀ n, Measure.map (T n) ρ = Measure.map (Q n) ν) :
       Measure.map S ρ = ν := by
   …

9. theorem OAI.Problem358.exists_map_of_approximating_mapL2_cauchy line 178

   Source documentation

   Completeness and target-law identification combined, without an optimality assertion.

   theorem exists_map_of_approximating_mapL2_cauchy [IsFiniteMeasure ρ] [IsFiniteMeasure ν]
       {T Q : ℕ → E d → E d}
       (hT : ∀ n, Measurable (T n)) (hQ : ∀ n, Measurable (Q n))
       (hTmem : ∀ n, MemLp (T n) 2 ρ)
       (hC : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N,
         mapL2Dist ρ (T m) (T n) < ε)
       (hQlim : ∀ᵐ y ∂ν, Tendsto (fun n => Q n y) atTop (𝓝 y))
       (hmap : ∀ n, Measure.map (T n) ρ = Measure.map (Q n) ν) :
       ∃ S : E d → E d, Measurable S ∧ MemLp S 2 ρ ∧ Measure.map S ρ = ν ∧
         Tendsto (fun n => mapL2Dist ρ (T n) S) atTop (𝓝 0) := by
   …