OAI/GroupTheory/SimpleAmenable/RandomFields/CompactSignalEnergy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.compactSignal_energy line 16
  2. def OAI.SimpleAmenable.sourceDyadicMass line 41
  3. theorem OAI.SimpleAmenable.sourceDyadicWeight_nonneg line 44
  4. theorem OAI.SimpleAmenable.sourceDyadicMass_nonneg line 47
  5. theorem OAI.SimpleAmenable.sourceDyadicMass_tendsto line 50
  6. theorem OAI.SimpleAmenable.sourceDyadic_radius_eventually line 73
  7. theorem OAI.SimpleAmenable.sourceDyadic_scale_bounds line 77
  8. theorem OAI.SimpleAmenable.finiteL2Norm_sum line 97
  9. theorem OAI.SimpleAmenable.finite_weighted_resolvent line 105
  10. theorem OAI.SimpleAmenable.finite_support_error_energy line 139
  11. theorem OAI.SimpleAmenable.finiteL2Norm_le_of_energy line 157