Flat.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Selecting a flat coefficient

lemma OAI.FourierLLogL.Dyadic.Thermal.flat_selection line 13

Source documentation

Find λ after the width estimate.

lemma flat_selection (D : ℝ) (hD : 1 ≤ D) :
    ∀ᶠ j : ℕ in atTop, ∀ (M : ℕ) (A B : Form M), 0 ≤ A → 0 ≤ B →
      ∀ t : ℝ, t ≤ D*height j →
        F (A+long j • B)-F A ≤ 400*t →
      ∃ c : ℝ, height j * H j^200 ≤ c ∧ H j^140*c ≤ long j ∧
        flat (H j) (plateErr j) A (c • B) ∧
        F (A+c • B)-F A ≤ 400*t ∧
        (label (A+c • B)).Ex (form B) ≤ 400*t/c := by
…

Mentions: OAI.FourierLLogL.Dyadic.Thermal.Form, OAI.FourierLLogL.Dyadic.Thermal.F, OAI.FourierLLogL.Dyadic.Thermal.H, OAI.FourierLLogL.Dyadic.Thermal.flat, OAI.FourierLLogL.Dyadic.Thermal.plateErr, OAI.FourierLLogL.Dyadic.Thermal.label, OAI.FourierLLogL.Dyadic.Thermal.form