OAI/Analysis/LipschitzHilbert/Estimates/ReferenceException.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The measurable planar exceptional set attached to one reference top.

  1. def OAI.LipschitzHilbert.SlopeBox.referenceException line 15
  2. theorem OAI.LipschitzHilbert.SlopeBox.measurableSet_referenceException line 19
  3. theorem OAI.LipschitzHilbert.SlopeBox.referenceException_measure_bound line 24
  4. theorem OAI.LipschitzHilbert.SlopeBox.count_le_outside_referenceException line 43

    Source documentation

    At every significant point outside this fixed exceptional set, the reference-line count is below the chosen threshold.

    theorem count_le_outside_referenceException (T : SlopeBox) (N : ℝ × ℝ → ℝ≥0∞)
    {K lambda : ℝ} {z : ℝ × ℝ} (hz : T.radius z ≤ K)
    (hout : z ∉ T.referenceException N K lambda) :
    N ((T.referenceChart.symm z).2, z.1) ≤ ENNReal.ofReal lambda := by
…

    Mentions: OAI.LipschitzHilbert.SlopeBox