OAI/Analysis/Brenier/SharpRectangle.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem358.rectCoordBox line 11

   Source documentation

   A coordinate box, expressed in the Euclidean-space model used by the challenge.

   def rectCoordBox {d : ℕ} (s : Fin d → Set ℝ) : Set (E d) :=
   …

2. lemma OAI.Problem358.rectCoordBox_measurable line 14
3. lemma OAI.Problem358.rectCoordBox_volume line 23
4. lemma OAI.Problem358.rect_cube_eq line 35
5. lemma OAI.Problem358.rect_cube_volume line 40
6. lemma OAI.Problem358.rectCoordBox_uniform_mass line 44
7. def OAI.Problem358.sharpRectIntervals line 61

   Source documentation

   A thin rectangle contained in the region where the two sharpness maps disagree.

   def sharpRectIntervals {d : ℕ} (i j : Fin d) (a b : ℝ) (k : Fin d) : Set ℝ :=
   …

8. def OAI.Problem358.sharpRectangle line 66
9. lemma OAI.Problem358.sharpRectIntervals_measurable line 69
10. lemma OAI.Problem358.sharpRectIntervals_subset line 74
11. lemma OAI.Problem358.sharpRectangle_mass line 85
12. lemma OAI.Problem358.sharpRectangle_real_mass line 122
13. lemma OAI.Problem358.sharpRectangle_measurable line 128
14. lemma OAI.Problem358.sharpRectangle_subset_cube line 132
15. lemma OAI.Problem358.sharpRectangle_subset_disagreement line 137
16. lemma OAI.Problem358.rect_integral_ge_measure line 153

    Source documentation

    Integrate a unit lower bound on a finite-measure set. No global finiteness is needed.

    lemma rect_integral_ge_measure {X : Type*} [MeasurableSpace X]
        {ρ : Measure X} {R : Set X} {f : X → ℝ}
        (hR : MeasurableSet R) (hfinite : ρ R < ∞) (hf : Integrable f ρ)
        (hnonneg : ∀ x, 0 ≤ f x) (hbound : ∀ x ∈ R, 1 ≤ f x) :
        ρ.real R ≤ ∫ x, f x ∂ρ := by
    …

17. lemma OAI.Problem358.sharpRectangle_integral_lower line 167
18. lemma OAI.Problem358.sharpRectangle_mapL2_lower line 183
19. lemma OAI.Problem358.Sharpness.slabMap_norm_sq_difference_le line 202
20. lemma OAI.Problem358.Sharpness.integrable_slabMap_norm_sq_difference line 211
21. lemma OAI.Problem358.Sharpness.slabMap_unit_lower_on_disagreement line 222
22. theorem OAI.Problem358.Sharpness.slabMap_mapL2_lower line 235

    Source documentation

    A coarse lower bound sufficient for the sharp exponent, with no symmetric-difference area calculation needed.

    theorem slabMap_mapL2_lower {d : ℕ} (i j : Fin d) (hij : i ≠ j)
        {a b : ℝ} (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b / 2 ≤ 1)
        :
        Real.sqrt (b / 16) ≤ mapL2Dist (uniformMeasure (cube d))
          (slabMap i j a 0) (slabMap i j a b) := by
    …

    Mentions: OAI.Problem358.Sharpness.slabMap