OAI/MeasureTheory/FalconerCompletion/Angular/InverseAdd.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Angular cutoffs and derivative estimates.

  1. lemma OAI.CurrentFalconer.MonotoneShell.inverse_add line 22
  2. lemma OAI.CurrentFalconer.MonotoneShell.inverse_smul line 28
  3. lemma OAI.CurrentFalconer.MonotoneShell.inverse_sub line 35
  4. def OAI.CurrentFalconer.MonotoneShell.complexMultiplier line 40
  5. lemma OAI.CurrentFalconer.MonotoneShell.complexMultiplier_continuous line 42
  6. lemma OAI.CurrentFalconer.MonotoneShell.complexMultiplier_zero line 44
  7. lemma OAI.CurrentFalconer.MonotoneShell.complexMultiplier_memLp line 50
  8. lemma OAI.CurrentFalconer.MonotoneShell.complexMultiplier_decompose line 54
  9. lemma OAI.CurrentFalconer.MonotoneShell.complexMultiplier_positive line 63
  10. lemma OAI.CurrentFalconer.MonotoneShell.complexMultiplier_sub line 67
  11. def OAI.CurrentFalconer.MonotoneShell.signedConv line 80
  12. def OAI.CurrentFalconer.MonotoneShell.complexConv line 83
  13. lemma OAI.CurrentFalconer.MonotoneShell.signedConv_L1 line 85
  14. lemma OAI.CurrentFalconer.MonotoneShell.complexConv_integrable line 98
  15. lemma OAI.CurrentFalconer.MonotoneShell.complexConv_L1_bound line 100
  16. lemma OAI.CurrentFalconer.MonotoneShell.complexConv_inverse line 122
  17. lemma OAI.CurrentFalconer.MonotoneShell.complexConv_positive line 131
  18. lemma OAI.CurrentFalconer.MonotoneShell.complexConv_sub line 136