OAI/Analysis/LipschitzHilbert/Estimates/FiniteEnergySchur.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite weighted energy summation for the smooth/dyadic comparison.

  1. theorem OAI.LipschitzHilbert.weighted_sum_norm_square line 15
  2. theorem OAI.LipschitzHilbert.weighted_integral_sum_square line 24
  3. theorem OAI.LipschitzHilbert.finite_energy_schur line 46