OAI/Analysis/FourierExtension/AutomaticBound.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Automatic boundedness and integral kernels on Lp spaces.

  1. def OAI.DiagonalExtension.AutomaticBound.pointwiseLpMap line 30
  2. theorem OAI.DiagonalExtension.AutomaticBound.continuous_pointwiseLpMap line 44
  3. theorem OAI.DiagonalExtension.AutomaticBound.exists_bound line 65
  4. lemma OAI.DiagonalExtension.KernelLp.integral_norm_le_lp line 88
  5. lemma OAI.DiagonalExtension.KernelLp.integrable_kernel line 106
  6. def OAI.DiagonalExtension.KernelLp.evalLinear line 111
  7. lemma OAI.DiagonalExtension.KernelLp.norm_evalLinear_le line 130
  8. def OAI.DiagonalExtension.KernelLp.eval line 139
  9. lemma OAI.DiagonalExtension.KernelLp.eval_apply line 144