OAI/Analysis/LipschitzHilbert/Trees/SourceThreeGridMaximal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

An actual interval maximal majorant built from three nested grids. The exceptional set is independent of the real interval parameters.

  1. abbrev OAI.LipschitzHilbert.DyadicLineGrid.GridChoice line 14
  2. def OAI.LipschitzHilbert.DyadicLineGrid.threeGridMaximal line 16
  3. theorem OAI.LipschitzHilbert.DyadicLineGrid.gridChoice_card line 19
  4. theorem OAI.LipschitzHilbert.DyadicLineGrid.threeGridMaximal_nonneg line 22
  5. theorem OAI.LipschitzHilbert.DyadicLineGrid.threeGridMaximal_measurable line 26
  6. theorem OAI.LipschitzHilbert.DyadicLineGrid.allDyadicMaximal_le_three line 29
  7. theorem OAI.LipschitzHilbert.DyadicLineGrid.threeGridMaximal_energy line 33
  8. theorem OAI.LipschitzHilbert.DyadicLineGrid.interval_average_le_threeGridMaximal line 52

    Source documentation

    All real intervals containing a point are controlled simultaneously, not merely an a.e. set chosen separately for each interval.

    theorem interval_average_le_threeGridMaximal {f : ℝ → ℝ}
    (hf : MemLp f 2 volume) (hf0 : ∀ x, 0≤f x) :
    ∀ᵐ x ∂volume, ∀ c r : ℝ, 0<r → x∈Icc (c-r) (c+r) →
      (∫ y in Icc (c-r) (c+r), f y)/(2*r)≤6*threeGridMaximal f x := by
…

    Mentions: OAI.LipschitzHilbert.DyadicLineGrid.threeGridMaximal