OAI/Analysis/FourierLLogL/Weak/Modular.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The Luxemburg gauge for the Fourier convergence class

  1. def OAI.FourierLLogL.priceΦ line 11
  2. def OAI.FourierLLogL.modBill line 12
  3. def OAI.FourierLLogL.luxSet line 13
  4. def OAI.FourierLLogL.luxNorm line 14
  5. lemma OAI.FourierLLogL.Weak.p_nonneg line 20
  6. lemma OAI.FourierLLogL.Weak.p_zero line 22
  7. lemma OAI.FourierLLogL.Weak.p_mono line 23
  8. def OAI.FourierLLogL.Weak.slopeΦ line 28
  9. lemma OAI.FourierLLogL.Weak.p_support line 29
  10. lemma OAI.FourierLLogL.Weak.price_convex line 47

    Source documentation

    Average of finitely many entries.

    lemma price_convex {ι : Type*} [Fintype ι] [Nonempty ι] (f : ι → ℂ) :
    let a : ℝ := Fintype.card ι
…
  11. lemma OAI.FourierLLogL.Weak.scale_admit line 69

    Source documentation

    Scalar comparison under every finite dilation.

    lemma scale_admit (a : ℝ) (ha : 0 ≤ a) :
    ∃ c : ℝ, 0 ≤ c ∧ ∀ x, 0 ≤ x → priceΦ (a*x) ≤ c*priceΦ x := by
…

    Mentions: OAI.FourierLLogL.priceΦ

  12. def OAI.FourierLLogL.Weak.Young line 84
  13. def OAI.FourierLLogL.Weak.inside line 85
  14. lemma OAI.FourierLLogL.Weak.young_meas line 87
  15. lemma OAI.FourierLLogL.Weak.mem_dilate line 93
  16. lemma OAI.FourierLLogL.Weak.mod_unit line 107
  17. lemma OAI.FourierLLogL.Weak.sum_inside line 110