OAI/Analysis/FourierLLogL/Weak/Layers.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.FourierLLogL.Weak.feeSummed line 15

    Source documentation

    allocate an integral for the good-part majorant, uniformly on modular ball

    lemma feeSummed (h : inside f) :
    (∑' j : ℕ,(2:ℝ)^(j+1)*heightLayerMass f j) ≤ 1 := by
…

    Mentions: OAI.FourierLLogL.Weak.inside, OAI.FourierLLogL.heightLayerMass

  2. def OAI.FourierLLogL.Weak.piece line 40
  3. def OAI.FourierLLogL.Weak.grit line 43
  4. lemma OAI.FourierLLogL.Weak.grit_pos line 44
  5. lemma OAI.FourierLLogL.Weak.grits line 45
  6. lemma OAI.FourierLLogL.Weak.grit_height line 51
  7. def OAI.FourierLLogL.Weak.allowance line 69
  8. lemma OAI.FourierLLogL.Weak.taxpayer line 72
  9. def OAI.FourierLLogL.Weak.tollMax line 96
  10. lemma OAI.FourierLLogL.Weak.toll_bound line 97
  11. lemma OAI.FourierLLogL.Weak.paid_transform line 114