SharpTargets.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem358.sharpAxis0 line 13
Source documentation
The first coordinate used in the sharpness construction.
```
def sharpAxis0 (d : ℕ) (hd : 2 ≤ d) : Fin d := ⟨0, by omega⟩
```
def OAI.Problem358.sharpAxis1 line 16
Source documentation
The transverse coordinate used in the sharpness construction.
```
def sharpAxis1 (d : ℕ) (hd : 2 ≤ d) : Fin d := ⟨1, by omega⟩
```
def OAI.Problem358.sharpAtoms line 19
Source documentation
The two fixed outer slopes and the variable central slope.
```
def sharpAtoms (d : ℕ) (hd : 2 ≤ d) (b : ℝ) : Fin 3 → E d :=
…
```
def OAI.Problem358.sharpWeights line 25
Source documentation
All three target masses are independent of the transverse slope.
```
def sharpWeights (a : ℝ) : Fin 3 → ℝ≥0∞ :=
…
```
def OAI.Problem358.sharpTarget line 29
Source documentation
The common three-atom target family; use b = 0 and b = a / 2.
```
def sharpTarget (d : ℕ) (hd : 2 ≤ d) (a b : ℝ) : Measure (E d) :=
…
```
lemma OAI.Problem358.sharpAtoms_injective line 32
lemma OAI.Problem358.sharpAtoms_mem_cube line 39
lemma OAI.Problem358.sharpWeights_pos line 44
lemma OAI.Problem358.sharpWeights_sum line 48
lemma OAI.Problem358.sharpTarget_hasExactlyThreeAtoms line 57
lemma OAI.Problem358.sharpTarget_isProbabilityMeasure line 64
lemma OAI.Problem358.sharpTarget_isSupported line 70
lemma OAI.Problem358.sharpTarget_apply_zero line 76
Source documentation
The zero atom distinguishes the two sharpness targets.
```
lemma sharpTarget_apply_zero (d : ℕ) (hd : 2 ≤ d) (a b : ℝ) :
    sharpTarget d hd a b {0} = if b = 0 then ENNReal.ofReal a else 0 := by
…
```
Mentions: OAI.Problem358.sharpTarget
lemma OAI.Problem358.sharpTarget_ne line 82
lemma OAI.Problem358.sharpTarget_ae_axis1_zero line 95
Source documentation
All source atoms lie in the transverse zero-coordinate hyperplane.
```
lemma sharpTarget_ae_axis1_zero (d : ℕ) (hd : 2 ≤ d) (a : ℝ) :
    ∀ᵐ x ∂sharpTarget d hd a 0, x (sharpAxis1 d hd) = 0 := by
…
```
Mentions: OAI.Problem358.sharpTarget, OAI.Problem358.sharpAxis1

lemma OAI.Problem358.sharpTarget_axis1_moment line 106

Source documentation

The target's transverse second moment only sees its central atom.

lemma sharpTarget_axis1_moment (d : ℕ) (hd : 2 ≤ d) (a b : ℝ) :
    (∫⁻ x, ENNReal.ofReal ((x (sharpAxis1 d hd)) ^ 2)
      ∂sharpTarget d hd a b) = ENNReal.ofReal a * ENNReal.ofReal (b ^ 2) := by
…

Mentions: OAI.Problem358.sharpAxis1, OAI.Problem358.sharpTarget

lemma OAI.Problem358.quadraticPlanCost_sharpMatching line 113

Source documentation

The atomwise matching plan changes only the central atom.

lemma quadraticPlanCost_sharpMatching (d : ℕ) (hd : 2 ≤ d) (a b : ℝ) :
    quadraticPlanCost (atomicMatchingPlan (sharpWeights a)
      (sharpAtoms d hd 0) (sharpAtoms d hd b)) =
      ENNReal.ofReal a * ENNReal.ofReal (b ^ 2) := by
…

Mentions: OAI.Problem358.atomicMatchingPlan, OAI.Problem358.sharpWeights, OAI.Problem358.sharpAtoms

lemma OAI.Problem358.wasserstein2_sharpTarget line 128

Source documentation

Exact quadratic Wasserstein distance for the three-atom sharpness family.

lemma wasserstein2_sharpTarget (d : ℕ) (hd : 2 ≤ d) {a : ℝ}
    (b : ℝ) (ha : 0 ≤ a) (ha1 : a ≤ 1) :
    wasserstein2 (sharpTarget d hd a 0) (sharpTarget d hd a b) =
      Real.sqrt (a * b ^ 2) := by
…

Mentions: OAI.Problem358.sharpTarget

lemma OAI.Problem358.wasserstein2_sharpTarget_pos line 145

Source documentation

Nonzero transverse displacement gives strictly positive target distance.

lemma wasserstein2_sharpTarget_pos (d : ℕ) (hd : 2 ≤ d) {a b : ℝ}
    (ha : 0 < a) (ha1 : a ≤ 1) (hb : b ≠ 0) :
    0 < wasserstein2 (sharpTarget d hd a 0) (sharpTarget d hd a b) := by
…

Mentions: OAI.Problem358.sharpTarget

lemma OAI.Problem358.wasserstein2_sharpTarget_half line 152

Source documentation

The standard choice b = a / 2 has squared transport cost a^3 / 4.

lemma wasserstein2_sharpTarget_half (d : ℕ) (hd : 2 ≤ d) {a : ℝ}
    (ha : 0 ≤ a) (ha1 : a ≤ 1) :
    wasserstein2 (sharpTarget d hd a 0) (sharpTarget d hd a (a / 2)) =
      Real.sqrt (a ^ 3 / 4) := by
…

Mentions: OAI.Problem358.sharpTarget