OAI/Analysis/LipschitzHilbert/Estimates/IntervalPoincare.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The interval energy estimate needed for the low-frequency part of the smooth-convolution versus cell-average comparison.

  1. theorem OAI.LipschitzHilbert.integral_square_le_mass_mul_square line 16
  2. theorem OAI.LipschitzHilbert.interval_pair_energy line 32
  3. theorem OAI.LipschitzHilbert.norm_sub_mean_le line 65
  4. theorem OAI.LipschitzHilbert.interval_mean_energy line 82

    Source documentation

    Pointwise Poincaré on one interval, with the actual integral mean.

    theorem interval_mean_energy {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [CompleteSpace E] (f : ℝ → E) {a b : ℝ} (hab : a < b)
    (hf : ∀ x ∈ Icc a b, DifferentiableAt ℝ f x)
    (hd : MemLp (deriv f) 2 (volume.restrict (Icc a b)))
    {x : ℝ} (hx : x ∈ Icc a b) :
    ‖f x - (b - a)⁻¹ • ∫ y in Icc a b, f y‖ ^ 2 ≤
      (b - a) * ∫ y in Icc a b, ‖deriv f y‖ ^ 2 := by
…
  5. theorem OAI.LipschitzHilbert.interval_poincare line 109

    Source documentation

    Integrated Poincaré with the interval length squared, independent of the dimension of the Hilbert packet space.

    theorem interval_poincare {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [CompleteSpace E] (f : ℝ → E) {a b : ℝ} (hab : a < b)
    (hf : ∀ x ∈ Icc a b, DifferentiableAt ℝ f x)
    (hd : MemLp (deriv f) 2 (volume.restrict (Icc a b))) :
    (∫ x in Icc a b, ‖f x - (b - a)⁻¹ • ∫ y in Icc a b, f y‖ ^ 2) ≤
      (b - a) ^ 2 * ∫ x in Icc a b, ‖deriv f x‖ ^ 2 := by
…
  6. theorem OAI.LipschitzHilbert.interval_poincare_Ico line 126