Sharpness.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.exists_pos_lt_rpow_lt line 13

Source documentation

A positive real power can be made arbitrarily small at a positive argument.

theorem exists_pos_lt_rpow_lt {p ε δ : ℝ}
    (hp : 0 < p) (hε : 0 < ε) (hδ : 0 < δ) :
    ∃ t : ℝ, 0 < t ∧ t < ε ∧ t ^ p < δ := by
…

theorem OAI.Problem358.exists_cubic_scaling_violation line 28
Source documentation
Scalar mechanism behind the sharp one-third exponent: cubic transport displacement cannot control linear map displacement with any exponent greater than one third.
```
theorem exists_cubic_scaling_violation {α C A B ε : ℝ}
    (hα : (1 / 3 : ℝ) < α) (hC : 0 < C) (hA : 0 < A)
    (hB : 0 < B) (hε : 0 < ε) :
    ∃ t : ℝ, 0 < t ∧ t < ε ∧ C * (A * t ^ 3) ^ α < B * t := by
…
```

theorem OAI.Problem358.exists_sharpness_parameter line 54

Source documentation

The exact one-dimensional numerical inequality used by the three-plane example, with the manuscript parameter a and b = a / 2.

theorem exists_sharpness_parameter {α C : ℝ}
    (hα : (1 / 3 : ℝ) < α) (hC : 0 < C) :
    ∃ a : ℝ, 0 < a ∧ a < 1 / 2 ∧
      C * (Real.sqrt (a * (a / 2) ^ 2)) ^ α <
        Real.sqrt (a / 4 + a * (a / 2) ^ 2) := by
…

theorem OAI.Problem358.exists_sharpness_parameter_of_lower_bound line 75
Source documentation
A lower bound proportional to sqrt a, rather than the exact map-distance formula, is already sufficient for sharpness. This permits a simple rectangular disagreement set.
```
theorem exists_sharpness_parameter_of_lower_bound {α C D : ℝ}
    (hα : (1 / 3 : ℝ) < α) (hC : 0 < C) (hD : 0 < D) :
    ∃ a : ℝ, 0 < a ∧ a < 1 / 2 ∧
      C * (Real.sqrt (a * (a / 2) ^ 2)) ^ α < Real.sqrt (D * a) := by
…
```

theorem OAI.Problem358.exists_sharpness_rectangle_parameter line 100

Source documentation

A conservative rectangular lower bound still gives the sharp one-third obstruction.

theorem exists_sharpness_rectangle_parameter {α C : ℝ}
    (hα : (1 / 3 : ℝ) < α) (hC : 0 < C) :
    ∃ a : ℝ, 0 < a ∧ a < 1 / 2 ∧
      C * (Real.sqrt (a * (a / 2) ^ 2)) ^ α < Real.sqrt (a / 32) := by
…

structure OAI.Problem358.SharpnessBoundsExample line 119
Source documentation
Transport data sufficient for sharpness, needing bounds rather than exact distances.
```
structure SharpnessBoundsExample (d : ℕ) (a : ℝ) where
…
```

theorem OAI.Problem358.one_third_exponent_is_sharp_of_bounds_examples line 138

Source documentation

Rectangle-mass lower bounds suffice to conclude the exact sharpness assertion.

theorem one_third_exponent_is_sharp_of_bounds_examples (d : ℕ)
    (examples : ∀ a : ℝ, 0 < a → a < 1 / 2 → Nonempty (SharpnessBoundsExample d a)) :
    ∀ α : ℝ, (1 / 3 : ℝ) < α → ∀ C : ℝ, 0 < C →
      ∃ (μ ν : Measure (E d)) (Tμ Tν : E d → E d),
        IsProbabilityMeasure μ ∧ IsProbabilityMeasure ν ∧
        IsSupported μ (cube d) ∧ IsSupported ν (cube d) ∧
        HasExactlyThreeAtoms μ (cube d) ∧ HasExactlyThreeAtoms ν (cube d) ∧
        μ ≠ ν ∧
        IsUniqueQuadraticOptimalMap (uniformMeasure (cube d)) μ Tμ ∧
        IsUniqueQuadraticOptimalMap (uniformMeasure (cube d)) ν Tν ∧
        0 < wasserstein2 μ ν ∧
        C * Real.rpow (wasserstein2 μ ν) α <
…

Mentions: OAI.Problem358.SharpnessBoundsExample

def OAI.Problem358.sharpnessBoundsExample line 170
Source documentation
The explicit cube maps satisfy a conservative sharpness certificate. This construction uses a small rectangle of disagreement, not the exact L² formula.
```
def sharpnessBoundsExample (d : ℕ) (hd : 2 ≤ d) (a : ℝ)
    (ha : 0 < a) (haSmall : a < 1 / 2) : SharpnessBoundsExample d a := by
…
```
Mentions: OAI.Problem358.SharpnessBoundsExample

theorem OAI.Problem358.one_third_exponent_is_sharp_via_rectangle line 201

Source documentation

An independent full proof of the sharpness conclusion using only coarse map-distance bounds.

theorem one_third_exponent_is_sharp_via_rectangle :
    ∀ (d : ℕ), 2 ≤ d → ∀ α : ℝ, (1 / 3 : ℝ) < α → ∀ C : ℝ, 0 < C → ∃ (μ ν : Measure (E d)) (Tμ Tν : E d → E d), IsProbabilityMeasure μ ∧ IsProbabilityMeasure ν ∧ IsSupported μ (cube d) ∧ IsSupported ν (cube d) ∧ HasExactlyThreeAtoms μ (cube d) ∧ HasExactlyThreeAtoms ν (cube d) ∧ μ ≠ ν ∧ IsUniqueQuadraticOptimalMap (uniformMeasure (cube d)) μ Tμ ∧ IsUniqueQuadraticOptimalMap (uniformMeasure (cube d)) ν Tν ∧ 0 < wasserstein2 μ ν ∧ C * Real.rpow (wasserstein2 μ ν) α < mapL2Dist (uniformMeasure (cube d)) Tμ Tν := by
…