OAI/Analysis/Brenier/MapDistance.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.mapL2Dist_self line 14
2. theorem OAI.Problem358.mapL2Dist_nonneg line 18
3. theorem OAI.Problem358.mapL2Dist_comm line 21
4. theorem OAI.Problem358.mapL2Dist_congr_ae line 25
5. theorem OAI.Problem358.mapL2Dist_eq_zero_of_ae_eq line 34
6. theorem OAI.Problem358.mapL2Dist_sq line 38
7. theorem OAI.Problem358.mapL2Dist_eq_zero_iff line 42
8. theorem OAI.Problem358.quadraticPlanCost_map_pair line 55
9. theorem OAI.Problem358.mapL2Dist_eq_sqrt_pair_cost line 61
10. theorem OAI.Problem358.mapL2Dist_eq_lpNorm line 70
11. theorem OAI.Problem358.mapL2Dist_eq_dist_toLp line 76
12. theorem OAI.Problem358.mapL2Dist_triangle line 81
13. theorem OAI.Problem358.integrable_norm_sub_sq_of_ae_bound line 96

    Source documentation

    A bounded nonnegative squared separation is integrable against a finite measure.

    theorem integrable_norm_sub_sq_of_ae_bound {ρ : Measure X} [IsFiniteMeasure ρ]
        {T S : X → V} (hT : Measurable T) (hS : Measurable S)
        {R : ℝ} (hbound : ∀ᵐ x ∂ρ, ‖T x - S x‖ ≤ R) :
        Integrable (fun x => ‖T x - S x‖ ^ 2) ρ := by
    …

14. theorem OAI.Problem358.ae_mem_of_map_compl_eq_zero line 108

    Source documentation

    Support of a pushforward pulls back to an almost-everywhere range condition.

    theorem ae_mem_of_map_compl_eq_zero {ρ : Measure X} {T : X → V}
        (hT : Measurable T) {Y : Set V} (hY : (Measure.map T ρ) Yᶜ = 0) :
        ∀ᵐ x ∂ρ, T x ∈ Y := by
    …

15. theorem OAI.Problem358.integrable_norm_sub_sq_of_ae_mem_bounded line 115

    Source documentation

    Two measurable maps with essentially bounded ranges have integrable squared separation.

    theorem integrable_norm_sub_sq_of_ae_mem_bounded {ρ : Measure X} [IsFiniteMeasure ρ]
        {T S : X → V} (hT : Measurable T) (hS : Measurable S)
        {Y Z : Set V} (hY : Bornology.IsBounded Y) (hZ : Bornology.IsBounded Z)
        (hTY : ∀ᵐ x ∂ρ, T x ∈ Y) (hSZ : ∀ᵐ x ∂ρ, S x ∈ Z) :
        Integrable (fun x => ‖T x - S x‖ ^ 2) ρ := by
    …

16. theorem OAI.Problem358.integrable_norm_sub_sq_of_map_compact line 127

    Source documentation

    Compact support of the two pushforwards suffices for the L² separation integral.

    theorem integrable_norm_sub_sq_of_map_compact {ρ : Measure X} [IsFiniteMeasure ρ]
        {T S : X → V} (hT : Measurable T) (hS : Measurable S)
        {Y Z : Set V} (hY : IsCompact Y) (hZ : IsCompact Z)
        (hTY : (Measure.map T ρ) Yᶜ = 0) (hSZ : (Measure.map S ρ) Zᶜ = 0) :
        Integrable (fun x => ‖T x - S x‖ ^ 2) ρ :=
    …

17. theorem OAI.Problem358.integral_norm_sub_sq_eq_zero_iff line 137

    Source documentation

    The squared L² separation integral vanishes exactly for a.e.-equal maps.

    theorem integral_norm_sub_sq_eq_zero_iff {ρ : Measure X} {T S : X → V}
        (hTS : Integrable (fun x => ‖T x - S x‖ ^ 2) ρ) :
        (∫ x, ‖T x - S x‖ ^ 2 ∂ρ) = 0 ↔ T =ᵐ[ρ] S := by
    …

18. theorem OAI.Problem358.exists_mapL2Dist_limit line 156
19. theorem OAI.Problem358.exists_subseq_tendsto_ae_of_mapL2Dist_tendsto_zero line 175
20. theorem OAI.Problem358.ae_mem_of_mapL2Dist_tendsto_zero line 193
21. theorem OAI.Problem358.exists_mapL2Dist_limit_in_closed line 205
22. theorem OAI.Problem358.tendsto_mapL2Dist_of_tendsto line 217

    Source documentation

    Map distance is continuous under L² convergence of each endpoint.

    theorem tendsto_mapL2Dist_of_tendsto {ι : Type*} {l : Filter ι}
        {T S : ι → E d → E d} {T₀ S₀ : E d → E d}
        (hT : ∀ n, MemLp (T n) 2 ρ) (hS : ∀ n, MemLp (S n) 2 ρ)
        (hT₀ : MemLp T₀ 2 ρ) (hS₀ : MemLp S₀ 2 ρ)
        (hTlim : Tendsto (fun n => mapL2Dist ρ (T n) T₀) l (𝓝 0))
        (hSlim : Tendsto (fun n => mapL2Dist ρ (S n) S₀) l (𝓝 0)) :
        Tendsto (fun n => mapL2Dist ρ (T n) (S n)) l (𝓝 (mapL2Dist ρ T₀ S₀)) := by
    …

23. theorem OAI.Problem358.graphPlan_eq_iff_ae_eq line 242

    Source documentation

    The graph plan of a measurable map remembers its almost-everywhere class.

    theorem graphPlan_eq_iff_ae_eq {d : ℕ} {ρ : Measure (E d)}
        {T S : E d → E d} (hT : Measurable T) (hS : Measurable S) :
        graphPlan ρ T = graphPlan ρ S ↔ T =ᵐ[ρ] S := by
    …

24. theorem OAI.Problem358.graphPlan_isCoupling line 261

    Source documentation

    A measurable transport of a probability source defines a coupling with its law.

    theorem graphPlan_isCoupling {d : ℕ} {ρ μ : Measure (E d)}
        [IsProbabilityMeasure ρ] {T : E d → E d}
        (hT : Measurable T) (hlaw : Measure.map T ρ = μ) :
        IsCoupling ρ μ (graphPlan ρ T) := by
    …

25. theorem OAI.Problem358.IsQuadraticOptimalMap.cost_eq line 275

    Source documentation

    All optimal maps for the same source and target have the same graph cost.

    theorem IsQuadraticOptimalMap.cost_eq {d : ℕ} {ρ μ : Measure (E d)}
        [IsProbabilityMeasure ρ] {T S : E d → E d}
        (hT : IsQuadraticOptimalMap ρ μ T) (hS : IsQuadraticOptimalMap ρ μ S) :
        quadraticPlanCost (graphPlan ρ T) = quadraticPlanCost (graphPlan ρ S) := by
    …

26. theorem OAI.Problem358.IsUniqueQuadraticOptimalMap.ae_eq_of_optimal line 284

    Source documentation

    Uniqueness among transport plans implies uniqueness of the map almost everywhere.

    theorem IsUniqueQuadraticOptimalMap.ae_eq_of_optimal {d : ℕ}
        {ρ μ : Measure (E d)} [IsProbabilityMeasure ρ] {T S : E d → E d}
        (hT : IsUniqueQuadraticOptimalMap ρ μ T)
        (hS : IsQuadraticOptimalMap ρ μ S) : T =ᵐ[ρ] S := by
    …

27. theorem OAI.Problem358.mapL2Dist_eq_of_optimal_maps line 293

    Source documentation

    Distances between unique optimal maps do not depend on selected representatives.

    theorem mapL2Dist_eq_of_optimal_maps {d : ℕ} {ρ μ ν : Measure (E d)}
        [IsProbabilityMeasure ρ] {T S T' S' : E d → E d}
        (hT : IsUniqueQuadraticOptimalMap ρ μ T)
        (hS : IsUniqueQuadraticOptimalMap ρ ν S)
        (hT' : IsQuadraticOptimalMap ρ μ T') (hS' : IsQuadraticOptimalMap ρ ν S') :
        mapL2Dist ρ T S = mapL2Dist ρ T' S' :=
    …

28. theorem OAI.Problem358.IsQuadraticOptimalMap.congr_ae line 302

    Source documentation

    Changing a measurable representative on a null set preserves optimality.

    theorem IsQuadraticOptimalMap.congr_ae {d : ℕ} {ρ μ : Measure (E d)}
        {T S : E d → E d} (hT : IsQuadraticOptimalMap ρ μ T)
        (hS : Measurable S) (hae : T =ᵐ[ρ] S) : IsQuadraticOptimalMap ρ μ S := by
    …

29. theorem OAI.Problem358.IsUniqueQuadraticOptimalMap.congr_ae line 313

    Source documentation

    Changing a measurable representative on a null set also preserves plan uniqueness.

    theorem IsUniqueQuadraticOptimalMap.congr_ae {d : ℕ} {ρ μ : Measure (E d)}
        {T S : E d → E d} (hT : IsUniqueQuadraticOptimalMap ρ μ T)
        (hS : Measurable S) (hae : T =ᵐ[ρ] S) :
        IsUniqueQuadraticOptimalMap ρ μ S := by
    …

30. theorem OAI.Problem358.StabilityLimit.real_bound_of_approximation line 335

    Source documentation

    A uniform power bound survives convergence when the input distances have only an asymptotic upper bound. This is enough for finite-target quantization.

    theorem real_bound_of_approximation
        {D W C α : ℝ} {Dₙ Wₙ ε : ℕ → ℝ}
        (hC : 0 ≤ C) (hα : 0 ≤ α) (hWₙ : ∀ n, 0 ≤ Wₙ n)
        (hD : Tendsto Dₙ atTop (𝓝 D)) (hε : Tendsto ε atTop (𝓝 0))
        (hupper : ∀ n, Wₙ n ≤ W + ε n)
        (hbound : ∀ n, Dₙ n ≤ C * Real.rpow (Wₙ n) α) :
        D ≤ C * Real.rpow W α := by
    …

31. theorem OAI.Problem358.StabilityLimit.dist_bound_of_approximation line 352

    Source documentation

    Metric version of the approximation closure step.

    theorem dist_bound_of_approximation {X : Type*} [PseudoMetricSpace X]
        {x y : X} {xₙ yₙ : ℕ → X} {W C α : ℝ} {Wₙ ε : ℕ → ℝ}
        (hC : 0 ≤ C) (hα : 0 ≤ α) (hWₙ : ∀ n, 0 ≤ Wₙ n)
        (hx : Tendsto xₙ atTop (𝓝 x)) (hy : Tendsto yₙ atTop (𝓝 y))
        (hε : Tendsto ε atTop (𝓝 0)) (hupper : ∀ n, Wₙ n ≤ W + ε n)
        (hbound : ∀ n, dist (xₙ n) (yₙ n) ≤ C * Real.rpow (Wₙ n) α) :
        dist x y ≤ C * Real.rpow W α := by
    …

32. theorem OAI.Problem358.StabilityLimit.one_third_dist_bound_of_approximation line 362

    Source documentation

    The exact exponent used by the stability target.

    theorem one_third_dist_bound_of_approximation {X : Type*} [PseudoMetricSpace X]
        {x y : X} {xₙ yₙ : ℕ → X} {W C : ℝ} {Wₙ ε : ℕ → ℝ}
        (hC : 0 ≤ C) (hWₙ : ∀ n, 0 ≤ Wₙ n)
        (hx : Tendsto xₙ atTop (𝓝 x)) (hy : Tendsto yₙ atTop (𝓝 y))
        (hε : Tendsto ε atTop (𝓝 0)) (hupper : ∀ n, Wₙ n ≤ W + ε n)
        (hbound : ∀ n, dist (xₙ n) (yₙ n) ≤ C * Real.rpow (Wₙ n) (1 / 3 : ℝ)) :
        dist x y ≤ C * Real.rpow W (1 / 3 : ℝ) := by
    …

33. theorem OAI.Problem358.StabilityLimit.tendsto_mapL2Dist line 375

    Source documentation

    Strong L² convergence in both arguments gives convergence of the map distance.

    theorem tendsto_mapL2Dist {T S : E d → E d} {Tₙ Sₙ : ℕ → E d → E d}
        (hT : MemLp T 2 ρ) (hS : MemLp S 2 ρ)
        (hTₙ : ∀ n, MemLp (Tₙ n) 2 ρ) (hSₙ : ∀ n, MemLp (Sₙ n) 2 ρ)
        (hlimT : Tendsto (fun n => mapL2Dist ρ (Tₙ n) T) atTop (𝓝 0))
        (hlimS : Tendsto (fun n => mapL2Dist ρ (Sₙ n) S) atTop (𝓝 0)) :
        Tendsto (fun n => mapL2Dist ρ (Tₙ n) (Sₙ n)) atTop (𝓝 (mapL2Dist ρ T S)) := by
    …

34. theorem OAI.Problem358.StabilityLimit.mapL2Dist_bound_of_approximation line 390

    Source documentation

    Passage from finite-target map bounds to a strong-L² limiting pair.

    theorem mapL2Dist_bound_of_approximation
        {T S : E d → E d} {Tₙ Sₙ : ℕ → E d → E d}
        {W C α : ℝ} {Wₙ ε : ℕ → ℝ}
        (hT : MemLp T 2 ρ) (hS : MemLp S 2 ρ)
        (hTₙ : ∀ n, MemLp (Tₙ n) 2 ρ) (hSₙ : ∀ n, MemLp (Sₙ n) 2 ρ)
        (hlimT : Tendsto (fun n => mapL2Dist ρ (Tₙ n) T) atTop (𝓝 0))
        (hlimS : Tendsto (fun n => mapL2Dist ρ (Sₙ n) S) atTop (𝓝 0))
        (hC : 0 ≤ C) (hα : 0 ≤ α) (hWₙ : ∀ n, 0 ≤ Wₙ n)
        (hε : Tendsto ε atTop (𝓝 0)) (hupper : ∀ n, Wₙ n ≤ W + ε n)
        (hbound : ∀ n, mapL2Dist ρ (Tₙ n) (Sₙ n) ≤ C * Real.rpow (Wₙ n) α) :
        mapL2Dist ρ T S ≤ C * Real.rpow W α := by
    …

35. theorem OAI.Problem358.StabilityLimit.one_third_bound_of_target_approximation line 405

    Source documentation

    Final one-third estimate under explicit finite approximation hypotheses.

    theorem one_third_bound_of_target_approximation
        {T S : E d → E d} {Tₙ Sₙ : ℕ → E d → E d}
        {μ ν : Measure (E d)} {μₙ νₙ : ℕ → Measure (E d)} {C : ℝ} {ε : ℕ → ℝ}
        (hT : MemLp T 2 ρ) (hS : MemLp S 2 ρ)
        (hTₙ : ∀ n, MemLp (Tₙ n) 2 ρ) (hSₙ : ∀ n, MemLp (Sₙ n) 2 ρ)
        (hlimT : Tendsto (fun n => mapL2Dist ρ (Tₙ n) T) atTop (𝓝 0))
        (hlimS : Tendsto (fun n => mapL2Dist ρ (Sₙ n) S) atTop (𝓝 0))
        (hC : 0 ≤ C) (hε : Tendsto ε atTop (𝓝 0))
        (hupper : ∀ n, wasserstein2 (μₙ n) (νₙ n) ≤ wasserstein2 μ ν + ε n)
        (hbound : ∀ n, mapL2Dist ρ (Tₙ n) (Sₙ n) ≤
          C * Real.rpow (wasserstein2 (μₙ n) (νₙ n)) (1 / 3 : ℝ)) :
        mapL2Dist ρ T S ≤ C * Real.rpow (wasserstein2 μ ν) (1 / 3 : ℝ) := by
    …

36. theorem OAI.Problem358.mapL2Dist_le_of_ae_bound line 430

    Source documentation

    On a probability source, an essential pointwise distance bound is an L² bound.

    theorem mapL2Dist_le_of_ae_bound {d : ℕ} {ρ : Measure (E d)}
        [IsProbabilityMeasure ρ] {T S : E d → E d}
        (hT : Measurable T) (hS : Measurable S) {M : ℝ} (hM : 0 ≤ M)
        (hbound : ∀ᵐ x ∂ρ, ‖T x - S x‖ ≤ M) :
        mapL2Dist ρ T S ≤ M := by
    …

37. theorem OAI.Problem358.mapL2Dist_le_of_ae_norm_bounds line 444

    Source documentation

    Uniform norm bounds on two maps give a uniform L² distance bound.

    theorem mapL2Dist_le_of_ae_norm_bounds {d : ℕ} {ρ : Measure (E d)}
        [IsProbabilityMeasure ρ] {T S : E d → E d}
        (hT : Measurable T) (hS : Measurable S) {R Q : ℝ}
        (hR : 0 ≤ R) (hQ : 0 ≤ Q)
        (hRT : ∀ᵐ x ∂ρ, ‖T x‖ ≤ R) (hQS : ∀ᵐ x ∂ρ, ‖S x‖ ≤ Q) :
        mapL2Dist ρ T S ≤ R + Q := by
    …

38. theorem OAI.Problem358.IsQuadraticOptimalMap.mapL2Dist_le_of_norm_bound line 455

    Source documentation

    The norms of optimal maps are controlled by a bound on the target supports.

    theorem IsQuadraticOptimalMap.mapL2Dist_le_of_norm_bound {d : ℕ}
        {ρ μ ν : Measure (E d)} [IsProbabilityMeasure ρ]
        {T S : E d → E d}
        (hT : IsQuadraticOptimalMap ρ μ T) (hS : IsQuadraticOptimalMap ρ ν S)
        {Y : Set (E d)} (hμ : IsSupported μ Y) (hν : IsSupported ν Y)
        {L : ℝ} (hL : 0 ≤ L) (hY : ∀ y ∈ Y, ‖y‖ ≤ L) :
        mapL2Dist ρ T S ≤ 2 * L := by
    …

39. theorem OAI.Problem358.mapL2Dist_eq_zero_iff_ae_of_compact line 475

    Source documentation

    Compact support of the pushforwards suffices for separation by map distance.

    theorem mapL2Dist_eq_zero_iff_ae_of_compact {d : ℕ} {ρ : Measure (E d)}
        [IsFiniteMeasure ρ] {T S : E d → E d} (hT : Measurable T) (hS : Measurable S)
        {Y Z : Set (E d)} (hY : IsCompact Y) (hZ : IsCompact Z)
        (hTY : IsSupported (Measure.map T ρ) Y) (hSZ : IsSupported (Measure.map S ρ) Z) :
        mapL2Dist ρ T S = 0 ↔ T =ᵐ[ρ] S :=
    …

40. theorem OAI.Problem358.mapL2Dist_pos_iff_not_ae line 483

    Source documentation

    Positive map distance is equivalent to distinct a.e. classes under integrability.

    theorem mapL2Dist_pos_iff_not_ae {d : ℕ} {ρ : Measure (E d)}
        {T S : E d → E d} (hTS : Integrable (fun x => ‖T x - S x‖ ^ 2) ρ) :
        0 < mapL2Dist ρ T S ↔ ¬ T =ᵐ[ρ] S := by
    …

41. theorem OAI.Problem358.mapL2Dist_pos_of_map_ne_of_compact line 491

    Source documentation

    Two unequal target laws force positive map distance for compact-supported maps.

    theorem mapL2Dist_pos_of_map_ne_of_compact {d : ℕ} {ρ : Measure (E d)}
        [IsFiniteMeasure ρ] {T S : E d → E d} (hT : Measurable T) (hS : Measurable S)
        {Y Z : Set (E d)} (hY : IsCompact Y) (hZ : IsCompact Z)
        (hTY : IsSupported (Measure.map T ρ) Y) (hSZ : IsSupported (Measure.map S ρ) Z)
        (hne : Measure.map T ρ ≠ Measure.map S ρ) : 0 < mapL2Dist ρ T S := by
    …

42. theorem OAI.Problem358.IsQuadraticOptimalMap.mapL2Dist_pos_of_ne line 503

    Source documentation

    Optimal maps to distinct compact-supported targets have positive map distance.

    theorem IsQuadraticOptimalMap.mapL2Dist_pos_of_ne {d : ℕ}
        {ρ μ ν : Measure (E d)} [IsFiniteMeasure ρ] {T S : E d → E d}
        (hT : IsQuadraticOptimalMap ρ μ T) (hS : IsQuadraticOptimalMap ρ ν S)
        {Y Z : Set (E d)} (hY : IsCompact Y) (hZ : IsCompact Z)
        (hμ : IsSupported μ Y) (hν : IsSupported ν Z) (hne : μ ≠ ν) :
        0 < mapL2Dist ρ T S := by
    …