OAI/Analysis/ModularRecovery/KernelContinuity.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Scalar kernel bounds, continuity, and spectral representations.

  1. lemma OAI.BoundedRecovery.continuous_kernelScalar line 17
  2. lemma OAI.BoundedRecovery.kernelScalar_even line 21
  3. lemma OAI.BoundedRecovery.kernelScalar_le_exp_neg_abs line 31
  4. lemma OAI.BoundedRecovery.hasDerivAt_kernelScalar line 42
  5. lemma OAI.BoundedRecovery.kernelScalar_deriv_bound line 53
  6. lemma OAI.BoundedRecovery.kernelScalar_lipschitz line 67
  7. lemma OAI.BoundedRecovery.integrable_exp_neg_abs_half line 73
  8. lemma OAI.BoundedRecovery.integrable_kernelScalar line 93
  9. def OAI.BoundedRecovery.translatedKernel line 99
  10. lemma OAI.BoundedRecovery.translatedKernel_apply line 106
  11. lemma OAI.BoundedRecovery.norm_translatedKernel_le line 108
  12. lemma OAI.BoundedRecovery.continuous_translatedKernel line 114
  13. lemma OAI.BoundedRecovery.StandardModularData.modularKernel_sum line 135
  14. lemma OAI.BoundedRecovery.StandardModularData.norm_modularKernel_le line 144
  15. lemma OAI.BoundedRecovery.modularResolvent_sub_norm_le line 161
  16. lemma OAI.BoundedRecovery.continuous_modularResolvent line 179
  17. lemma OAI.BoundedRecovery.StandardModularData.continuous_modularKernel_xi line 193
  18. lemma OAI.BoundedRecovery.StandardModularData.continuous_modularKernel_apply line 205
  19. lemma OAI.BoundedRecovery.RealSpectralCalculus.halfGraph_calculus line 265
  20. lemma OAI.BoundedRecovery.translatedKernel_eq_mixed line 276
  21. lemma OAI.BoundedRecovery.StandardModularData.modularKernel_xi line 289