OAI/MeasureTheory/FalconerCompletion/Fourier/SignedVariationFinite.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Fourier kernels and oscillatory estimates.

  1. instance OAI.CurrentFalconer.MonotoneShell.signed_variation_finite line 16
  2. lemma OAI.CurrentFalconer.MonotoneShell.character_integrable line 19
  3. def OAI.CurrentFalconer.MonotoneShell.signedChar line 24
  4. def OAI.CurrentFalconer.MonotoneShell.complexChar line 26
  5. lemma OAI.CurrentFalconer.MonotoneShell.signed_integral_character line 28
  6. lemma OAI.CurrentFalconer.MonotoneShell.complexChar_eq_fourier line 50
  7. lemma OAI.CurrentFalconer.MonotoneShell.complexChar_continuous line 71
  8. lemma OAI.CurrentFalconer.MonotoneShell.complexChar_positive line 75
  9. lemma OAI.CurrentFalconer.MonotoneShell.complexChar_sub line 81
  10. lemma OAI.CurrentFalconer.MonotoneShell.real_variation_le line 87
  11. lemma OAI.CurrentFalconer.MonotoneShell.imag_variation_le line 94