CompactMeasure.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.integrable_of_continuousOn_of_ae_mem_compact line 19
Source documentation
Continuity only on a compact set of full measure suffices for integrability.
```
theorem integrable_of_continuousOn_of_ae_mem_compact
    (hK : IsCompact K) (hμ : ∀ᵐ x ∂μ, x ∈ K) (hf : ContinuousOn f K) :
    Integrable f μ := by
…
```

theorem OAI.Problem358.integrable_comp_of_continuousOn_of_map_ae_mem_compact line 27

Source documentation

The preceding result through a measurable pushforward.

theorem integrable_comp_of_continuousOn_of_map_ae_mem_compact
    {A : Type*} [MeasurableSpace A] {ρ : Measure A} [IsFiniteMeasure ρ]
    {T : A → X} (hT : Measurable T) (hK : IsCompact K)
    (hρ : ∀ᵐ x ∂Measure.map T ρ, x ∈ K) (hf : ContinuousOn f K) :
    Integrable (fun x => f (T x)) ρ := by
…

theorem OAI.Problem358.IsSupported.integrable_continuousOn line 37

Source documentation

Continuous-on-support functions are integrable for compactly supported finite measures.

theorem IsSupported.integrable_continuousOn
    {d : ℕ} {μ : Measure (E d)} [IsFiniteMeasure μ] {K : Set (E d)}
    (hμ : IsSupported μ K) (hK : IsCompact K)
    {F : Type*} [NormedAddCommGroup F] {f : E d → F} (hf : ContinuousOn f K) :
    Integrable f μ := by
…

theorem OAI.Problem358.integrable_comp_of_supported_map line 45

Source documentation

A continuous potential on a compact target is integrable after a measurable transport.

theorem integrable_comp_of_supported_map
    {d : ℕ} {A : Type*} [MeasurableSpace A] {ρ : Measure A} [IsFiniteMeasure ρ]
    {T : A → E d} (hT : Measurable T) {K : Set (E d)}
    (hK : IsCompact K) (hρ : IsSupported (Measure.map T ρ) K)
    {F : Type*} [NormedAddCommGroup F] {f : E d → F} (hf : ContinuousOn f K) :
    Integrable (fun x => f (T x)) ρ := by
…

theorem OAI.Problem358.IsCoupling.integrable_continuousOn_prod line 54

Source documentation

Every continuous function on the compact product support of a coupling is integrable.

theorem IsCoupling.integrable_continuousOn_prod
    {d : ℕ} {μ ν : Measure (E d)} {π : Measure (E d × E d)}
    (hπ : IsCoupling μ ν π) {K Y : Set (E d)}
    (hK : IsCompact K) (hY : IsCompact Y)
    (hμ : IsSupported μ K) (hν : IsSupported ν Y)
    {F : Type*} [NormedAddCommGroup F] {f : E d × E d → F}
    (hf : ContinuousOn f (K ×ˢ Y)) : Integrable f π := by
…

theorem OAI.Problem358.CompactIntegrability.ae_mem_of_supported_map line 90
Source documentation
A compact-supported pushforward puts the map in that compact set almost everywhere.
```
theorem ae_mem_of_supported_map (hT : Measurable T) (hY : IsCompact Y)
    (hTY : IsSupported (Measure.map T ρ) Y) : ∀ᵐ x ∂ρ, T x ∈ Y := by
…
```

theorem OAI.Problem358.CompactIntegrability.integrable_norm_pow_of_ae_mem line 96

Source documentation

Every natural moment of the norm of a compact-valued measurable map is integrable.

theorem integrable_norm_pow_of_ae_mem [IsFiniteMeasure ρ]
    (hT : Measurable T) (hY : IsCompact Y) (hTY : ∀ᵐ x ∂ρ, T x ∈ Y)
    (n : ℕ) : Integrable (fun x => ‖T x‖ ^ n) ρ := by
…

theorem OAI.Problem358.CompactIntegrability.integrable_norm_sq_of_supported_map line 106

Source documentation

Squared norm integrability from compact support of the pushforward.

theorem integrable_norm_sq_of_supported_map [IsFiniteMeasure ρ]
    (hT : Measurable T) (hY : IsCompact Y)
    (hTY : IsSupported (Measure.map T ρ) Y) :
    Integrable (fun x => ‖T x‖ ^ 2) ρ :=
…

theorem OAI.Problem358.CompactIntegrability.ae_mem_of_ae_tendsto line 113

Source documentation

An almost-everywhere limit of maps into a fixed compact set stays in that set.

theorem ae_mem_of_ae_tendsto {F : ℕ → E d → E d}
    (hY : IsCompact Y) (hFY : ∀ n, ∀ᵐ x ∂ρ, F n x ∈ Y)
    (hlim : ∀ᵐ x ∂ρ, Filter.Tendsto (fun n => F n x) Filter.atTop (𝓝 (T x))) :
    ∀ᵐ x ∂ρ, T x ∈ Y := by
…

theorem OAI.Problem358.CompactIntegrability.tendsto_integral_comp_of_ae_tendsto line 122

Source documentation

Compact range supplies the domination needed to pass to continuous test integrals.

theorem tendsto_integral_comp_of_ae_tendsto [IsFiniteMeasure ρ]
    {F : ℕ → E d → E d} (hF : ∀ n, Measurable (F n))
    (hY : IsCompact Y) (hFY : ∀ n, ∀ᵐ x ∂ρ, F n x ∈ Y)
    (hlim : ∀ᵐ x ∂ρ, Filter.Tendsto (fun n => F n x) Filter.atTop (𝓝 (T x)))
    {φ : E d → ℝ} (hφ : Continuous φ) :
    Filter.Tendsto (fun n => ∫ x, φ (F n x) ∂ρ) Filter.atTop
      (𝓝 (∫ x, φ (T x) ∂ρ)) := by
…

theorem OAI.Problem358.CompactIntegrability.tendsto_integral_sub_norm_sq_of_ae_tendsto line 142

Source documentation

Almost-everywhere convergence within a common compact range implies convergence of squared map distances. This is the bounded-convergence step in finite-target approximation.

theorem tendsto_integral_sub_norm_sq_of_ae_tendsto [IsFiniteMeasure ρ]
    {F : ℕ → E d → E d} (hF : ∀ n, Measurable (F n)) (hT : Measurable T)
    (hY : IsCompact Y) (hFY : ∀ n, ∀ᵐ x ∂ρ, F n x ∈ Y)
    (hlim : ∀ᵐ x ∂ρ, Filter.Tendsto (fun n => F n x) Filter.atTop (𝓝 (T x))) :
    Filter.Tendsto (fun n => ∫ x, ‖F n x - T x‖ ^ 2 ∂ρ) Filter.atTop (𝓝 0) := by
…

theorem OAI.Problem358.CompactIntegrability.tendsto_mapL2Dist_of_ae_tendsto line 168

Source documentation

Compact-range bounded convergence stated using the problem's exact map distance.

theorem tendsto_mapL2Dist_of_ae_tendsto [IsFiniteMeasure ρ]
    {F : ℕ → E d → E d} (hF : ∀ n, Measurable (F n)) (hT : Measurable T)
    (hY : IsCompact Y) (hFY : ∀ n, ∀ᵐ x ∂ρ, F n x ∈ Y)
    (hlim : ∀ᵐ x ∂ρ, Filter.Tendsto (fun n => F n x) Filter.atTop (𝓝 (T x))) :
    Filter.Tendsto (fun n => mapL2Dist ρ (F n) T) Filter.atTop (𝓝 0) := by
…

theorem OAI.Problem358.CompactIntegrability.map_eq_of_ae_tendsto_of_test_tendsto line 184

Source documentation

Identify a compact-range pointwise limit's law by continuous test integrals.

theorem map_eq_of_ae_tendsto_of_test_tendsto [IsFiniteMeasure ρ] [IsFiniteMeasure μ]
    (hF : ∀ n, Measurable (F n)) (hT : Measurable T)
    (hY : IsCompact Y) (hFY : ∀ n, ∀ᵐ x ∂ρ, F n x ∈ Y)
    (hlim : ∀ᵐ x ∂ρ, Tendsto (fun n => F n x) atTop (𝓝 (T x)))
    (htest : ∀ φ : E d → ℝ, Continuous φ →
      Tendsto (fun n => ∫ x, φ (F n x) ∂ρ) atTop (𝓝 (∫ y, φ y ∂μ))) :
    Measure.map T ρ = μ := by
…

theorem OAI.Problem358.CompactIntegrability.map_eq_of_ae_tendsto_of_map_eq_quantizers line 200

Source documentation

If the approximating maps have the laws of quantizers converging to the identity, the almost-everywhere limit has the original target law.

theorem map_eq_of_ae_tendsto_of_map_eq_quantizers [IsFiniteMeasure ρ] [IsFiniteMeasure μ]
    (hF : ∀ n, Measurable (F n)) (hT : Measurable T)
    (hQ : ∀ n, Measurable (Q n)) (hY : IsCompact Y)
    (hFY : ∀ n, ∀ᵐ x ∂ρ, F n x ∈ Y)
    (hQY : ∀ n, ∀ᵐ y ∂μ, Q n y ∈ Y)
    (hlim : ∀ᵐ x ∂ρ, Tendsto (fun n => F n x) atTop (𝓝 (T x)))
    (hQlim : ∀ᵐ y ∂μ, Tendsto (fun n => Q n y) atTop (𝓝 y))
    (hpush : ∀ n, Measure.map (F n) ρ = Measure.map (Q n) μ) :
    Measure.map T ρ = μ := by
…