OAI/Analysis/Brenier/MapTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.wasserstein2_map_le_mapL2Dist line 16

   Source documentation

   The common-source plan bounds transport distance by map distance.

   theorem wasserstein2_map_le_mapL2Dist [IsProbabilityMeasure ρ]
       (hT : Measurable T) (hS : Measurable S)
       (hInt : Integrable (fun x => ‖T x - S x‖ ^ 2) ρ) :
       wasserstein2 (Measure.map T ρ) (Measure.map S ρ) ≤ mapL2Dist ρ T S := by
   …

2. theorem OAI.Problem358.wasserstein2_le_mapL2Dist line 35

   Source documentation

   The same inequality for maps presented with specified pushforward laws.

   theorem wasserstein2_le_mapL2Dist [IsProbabilityMeasure ρ]
       {μ ν : Measure (E d)} (hT : Measurable T) (hS : Measurable S)
       (hμ : Measure.map T ρ = μ) (hν : Measure.map S ρ = ν)
       (hInt : Integrable (fun x => ‖T x - S x‖ ^ 2) ρ) :
       wasserstein2 μ ν ≤ mapL2Dist ρ T S := by
   …

3. theorem OAI.Problem358.exists_optimal_maps_wasserstein_bound_of_coupling_bounds line 58

   Source documentation

   Bounds from coupling-dependent optimal maps transfer to a single pair of maps before taking the cost infimum. Plan uniqueness makes the choice harmless.

   theorem exists_optimal_maps_wasserstein_bound_of_coupling_bounds
       {π₀ : Measure (E d × E d)} (hπ₀ : IsCoupling μ ν π₀)
       (hfinite : quadraticPlanCost π₀ ≠ ∞) {C α : ℝ}
       (hC : 0 ≤ C) (hα : 0 ≤ α)
       (hbound : ∀ π : Measure (E d × E d), IsCoupling μ ν π →
         quadraticPlanCost π ≠ ∞ →
         ∃ T S : E d → E d, IsUniqueQuadraticOptimalMap ρ μ T ∧
           IsUniqueQuadraticOptimalMap ρ ν S ∧
           mapL2Dist ρ T S ≤ C * Real.rpow (Real.sqrt (quadraticPlanCost π).toReal) α) :
       ∃ T S : E d → E d, IsUniqueQuadraticOptimalMap ρ μ T ∧
         IsUniqueQuadraticOptimalMap ρ ν S ∧
         mapL2Dist ρ T S ≤ C * Real.rpow (wasserstein2 μ ν) α := by
   …

4. theorem OAI.Problem358.exists_optimal_maps_bound_of_approximate_bounds line 81

   Source documentation

   Approximate estimates may also choose different unique optimal maps for every positive error. The limiting estimate needs neither a compactness argument nor convergence of these representatives.

   theorem exists_optimal_maps_bound_of_approximate_bounds
       {F : ℝ → ℝ} {w : ℝ} (hcont : ContinuousAt F w)
       (hbound : ∀ ε : ℝ, 0 < ε →
         ∃ T S : E d → E d, IsUniqueQuadraticOptimalMap ρ μ T ∧
           IsUniqueQuadraticOptimalMap ρ ν S ∧ mapL2Dist ρ T S ≤ F (w + ε)) :
       ∃ T S : E d → E d, IsUniqueQuadraticOptimalMap ρ μ T ∧
         IsUniqueQuadraticOptimalMap ρ ν S ∧ mapL2Dist ρ T S ≤ F w := by
   …