OAI/Analysis/Brenier/Potential.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem358.MaxPotential.potential line 15

   Source documentation

   A finite maximum of affine functions, with slopes y and intercepts c.

   def potential (y : ι → V) (c : ι → ℝ) (x : V) : ℝ :=
   …

2. theorem OAI.Problem358.MaxPotential.affine_le_potential line 18
3. theorem OAI.Problem358.MaxPotential.potential_le line 22
4. theorem OAI.Problem358.MaxPotential.affine_eq_potential line 26
5. theorem OAI.Problem358.MaxPotential.supporting_inequality line 31
6. theorem OAI.Problem358.MaxPotential.convexOn_potential line 37
7. theorem OAI.Problem358.MaxPotential.potential_sub_le line 49
8. theorem OAI.Problem358.MaxPotential.lipschitzWith_potential line 66
9. theorem OAI.Problem358.MaxPotential.continuous_potential line 78
10. theorem OAI.Problem358.MaxPotential.eventuallyEq_affine_of_strict line 88

    Source documentation

    A strict active affine piece remains active in a neighborhood.

    theorem eventuallyEq_affine_of_strict (y : ι → V) (c : ι → ℝ) (x : V) (i : ι)
        (h : ∀ j, j ≠ i → ⟪x, y j⟫ + c j < ⟪x, y i⟫ + c i) :
        potential y c =ᶠ[𝓝 x] (fun z => ⟪z, y i⟫ + c i) := by
    …

    Mentions: OAI.Problem358.MaxPotential.potential

11. theorem OAI.Problem358.MaxPotential.hasFDerivAt_of_strict line 106

    Source documentation

    At a strict active cell the derivative is its site's inner-product functional.

    theorem hasFDerivAt_of_strict (y : ι → V) (c : ι → ℝ) (x : V) (i : ι)
        (h : ∀ j, j ≠ i → ⟪x, y j⟫ + c j < ⟪x, y i⟫ + c i) :
        HasFDerivAt (potential y c) (innerSL ℝ (y i)) x := by
    …

    Mentions: OAI.Problem358.MaxPotential.potential

12. theorem OAI.Problem358.MaxPotential.potential_intercept_sub_le line 128
13. theorem OAI.Problem358.MaxPotential.norm_potential_intercept_sub_le line 141
14. theorem OAI.Problem358.MaxPotential.lipschitzWith_intercepts line 151
15. theorem OAI.Problem358.MaxPotential.norm_potential_le line 158
16. theorem OAI.Problem358.MaxPotential.integrable_potential line 175
17. theorem OAI.Problem358.MaxPotential.norm_integral_potential_sub_le line 184

    Source documentation

    Integrating the potential preserves its uniform intercept continuity.

    theorem norm_integral_potential_sub_le (y : ι → V) (c b : ι → ℝ)
        (hc : Integrable (potential y c) ρ) (hb : Integrable (potential y b) ρ) :
        ‖(∫ x, potential y c x ∂ρ) - ∫ x, potential y b x ∂ρ‖ ≤
          ‖c - b‖ * ρ.real Set.univ := by
    …

    Mentions: OAI.Problem358.MaxPotential.potential

18. theorem OAI.Problem358.MaxPotential.lipschitzWith_integral_potential line 195
19. theorem OAI.Problem358.MaxPotential.intercept_le_integral_potential line 204

    Source documentation

    The elementary coercivity estimate for each intercept coordinate.

    theorem intercept_le_integral_potential (y : ι → V) (c : ι → ℝ) (L : NNReal)
        (hy : ∀ i, ‖y i‖ ≤ L) (hρ : Integrable (fun x : V => ‖x‖) ρ) (i : ι) :
        c i ≤ (∫ x, potential y c x ∂ρ) + (L : ℝ) * ∫ x, ‖x‖ ∂ρ := by
    …

    Mentions: OAI.Problem358.MaxPotential.potential

20. theorem OAI.Problem358.MaxPotential.convexOn_intercepts line 241

    Source documentation

    Convexity in the intercept vector, as distinct from convexity in the source variable.

    theorem convexOn_intercepts (y : ι → V) (x : V) :
        ConvexOn ℝ Set.univ (fun c => potential y c x) := by
    …

    Mentions: OAI.Problem358.MaxPotential.potential

21. theorem OAI.Problem358.MaxPotential.convexOn_integral_potential line 260
22. theorem OAI.Problem358.MaxPotential.convexOn_integral_potential_sub_weighted_sum line 272

    Source documentation

    The complete normalized-cell variational objective is convex.

    theorem convexOn_integral_potential_sub_weighted_sum
        (ρ : Measure V) (y : ι → V) (m : ι → ℝ)
        (hint : ∀ c, Integrable (potential y c) ρ) :
        ConvexOn ℝ Set.univ
          (fun c => (∫ x, potential y c x ∂ρ) - ∑ i, m i * c i) := by
    …

    Mentions: OAI.Problem358.MaxPotential.potential

23. theorem OAI.Problem358.MaxPotential.eqOn_of_finite_ae_range line 315

    Source documentation

    A continuous function with finite essential range is constant on every connected subset of the measure's support.

    theorem eqOn_of_finite_ae_range (ρ : Measure V) {K : Set V}
        (hK : IsPreconnected K) (hKs : K ⊆ ρ.support)
        {f : V → ℝ} (hf : Continuous f) {A : Set ℝ} (hA : A.Finite)
        (hae : ∀ᵐ x ∂ρ, f x ∈ A) {x z : V} (hx : x ∈ K) (hz : z ∈ K) :
        f x = f z := by
    …

24. theorem OAI.Problem358.MaxPotential.intercept_sub_eq_of_common_selector line 333

    Source documentation

    If the same positive-mass selector is active for two finite affine potentials, then their intercept difference is constant on the index set.

    theorem intercept_sub_eq_of_common_selector (ρ : Measure V) {K : Set V}
        (hK : IsPreconnected K) (hKs : K ⊆ ρ.support)
        (hKae : ∀ᵐ x ∂ρ, x ∈ K) (y : ι → V) (c b : ι → ℝ) (k : V → ι)
        (hc : ∀ᵐ x ∂ρ, potential y c x = ⟪x, y (k x)⟫ + c (k x))
        (hb : ∀ᵐ x ∂ρ, potential y b x = ⟪x, y (k x)⟫ + b (k x))
        (hpos : ∀ i, ρ {x | k x = i} ≠ 0) (i j : ι) :
        c i - b i = c j - b j := by
    …

    Mentions: OAI.Problem358.MaxPotential.potential

25. theorem OAI.Problem358.MaxPotential.intercept_eq_of_common_selector line 360

    Source documentation

    Weighted normalization removes the common additive intercept constant.

    theorem intercept_eq_of_common_selector (ρ : Measure V) {K : Set V}
        (hK : IsPreconnected K) (hKs : K ⊆ ρ.support)
        (hKae : ∀ᵐ x ∂ρ, x ∈ K) (y : ι → V) (c b m : ι → ℝ) (k : V → ι)
        (hsum : ∑ i, m i = 1) (hc0 : ∑ i, m i * c i = 0)
        (hb0 : ∑ i, m i * b i = 0)
        (hc : ∀ᵐ x ∂ρ, potential y c x = ⟪x, y (k x)⟫ + c (k x))
        (hb : ∀ᵐ x ∂ρ, potential y b x = ⟪x, y (k x)⟫ + b (k x))
        (hpos : ∀ i, ρ {x | k x = i} ≠ 0) : c = b := by
    …

    Mentions: OAI.Problem358.MaxPotential.potential

26. theorem OAI.Problem358.MaxPotential.potential_midpoint_le line 383

    Source documentation

    Convexity of the maximum in its intercepts, at the midpoint.

    theorem potential_midpoint_le (y : ι → V) (c b : ι → ℝ) (x : V) :
        potential y (fun i => (c i + b i) / 2) x ≤
          (potential y c x + potential y b x) / 2 := by
    …

    Mentions: OAI.Problem358.MaxPotential.potential

27. theorem OAI.Problem358.MaxPotential.active_of_midpoint_eq line 393

    Source documentation

    Equality in midpoint convexity forces a strict active index at one endpoint also to be active at the other endpoint.

    theorem active_of_midpoint_eq (y : ι → V) (c b : ι → ℝ) (x : V) (k : ι)
        (hstrict : ∀ j, j ≠ k → ⟪x, y j⟫ + c j < ⟪x, y k⟫ + c k)
        (heq : potential y (fun i => (c i + b i) / 2) x =
          (potential y c x + potential y b x) / 2) :
        potential y b x = ⟪x, y k⟫ + b k := by
    …

    Mentions: OAI.Problem358.MaxPotential.potential

28. theorem OAI.Problem358.MaxPotential.ae_common_selector_of_integral_midpoint_eq line 414

    Source documentation

    Integrated midpoint equality upgrades a strict selector at the first endpoint to a common almost-everywhere selector.

    theorem ae_common_selector_of_integral_midpoint_eq (ρ : Measure V)
        (y : ι → V) (c b : ι → ℝ) (k : V → ι)
        (hc : Integrable (potential y c) ρ) (hb : Integrable (potential y b) ρ)
        (hm : Integrable (potential y (fun i => (c i + b i) / 2)) ρ)
        (hstrict : ∀ᵐ x ∂ρ, ∀ j, j ≠ k x →
          ⟪x, y j⟫ + c j < ⟪x, y (k x)⟫ + c (k x))
        (heq : (∫ x, potential y (fun i => (c i + b i) / 2) x ∂ρ) =
          ((∫ x, potential y c x ∂ρ) + ∫ x, potential y b x ∂ρ) / 2) :
        ∀ᵐ x ∂ρ, potential y b x = ⟪x, y (k x)⟫ + b (k x) := by
    …

    Mentions: OAI.Problem358.MaxPotential.potential

29. theorem OAI.Problem358.MaxPotential.integral_midpoint_eq_of_minimizers line 432

    Source documentation

    Two normalized minimizers have equality in integrated midpoint convexity.

    theorem integral_midpoint_eq_of_minimizers (ρ : Measure V)
        (y : ι → V) (c b m : ι → ℝ)
        (hc0 : ∑ i, m i * c i = 0) (hb0 : ∑ i, m i * b i = 0)
        (hint : ∀ a : ι → ℝ, Integrable (potential y a) ρ)
        (hcmin : ∀ a : ι → ℝ, (∑ i, m i * a i) = 0 →
          (∫ x, potential y c x ∂ρ) ≤ ∫ x, potential y a x ∂ρ)
        (hbmin : ∀ a : ι → ℝ, (∑ i, m i * a i) = 0 →
          (∫ x, potential y b x ∂ρ) ≤ ∫ x, potential y a x ∂ρ) :
        (∫ x, potential y (fun i => (c i + b i) / 2) x ∂ρ) =
          ((∫ x, potential y c x ∂ρ) + ∫ x, potential y b x ∂ρ) / 2 := by
    …

    Mentions: OAI.Problem358.MaxPotential.potential

30. theorem OAI.Problem358.MaxPotential.normalized_minimizer_unique line 462

    Source documentation

    Uniqueness of normalized intercept minimizers. The only geometric inputs are connected full support and almost-everywhere strictness of the chosen cells. No cell boundary differentiability or implicit-function theorem is required.

    theorem normalized_minimizer_unique (ρ : Measure V) {K : Set V}
        (hK : IsPreconnected K) (hKs : K ⊆ ρ.support)
        (hKae : ∀ᵐ x ∂ρ, x ∈ K) (y : ι → V) (c b m : ι → ℝ) (k : V → ι)
        (hsum : ∑ i, m i = 1) (hc0 : ∑ i, m i * c i = 0)
        (hb0 : ∑ i, m i * b i = 0)
        (hint : ∀ a : ι → ℝ, Integrable (potential y a) ρ)
        (hcmin : ∀ a : ι → ℝ, (∑ i, m i * a i) = 0 →
          (∫ x, potential y c x ∂ρ) ≤ ∫ x, potential y a x ∂ρ)
        (hbmin : ∀ a : ι → ℝ, (∑ i, m i * a i) = 0 →
          (∫ x, potential y b x ∂ρ) ≤ ∫ x, potential y a x ∂ρ)
        (hstrict : ∀ᵐ x ∂ρ, ∀ j, j ≠ k x →
          ⟪x, y j⟫ + c j < ⟪x, y (k x)⟫ + c (k x))
    …

    Mentions: OAI.Problem358.MaxPotential.potential