OAI/Analysis/ModularTheory/WeightedDensity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Removing the scalar exponential weight by bounded inverse cutoffs. This approximates ordinary L2 vectors by the actual finite-weight test functions.

  1. def OAI.WeakPureInfiniteness.inverseWeightFactor line 13
  2. lemma OAI.WeakPureInfiniteness.inverseWeightFactor_bound line 16
  3. lemma OAI.WeakPureInfiniteness.inverseWeightFactor_tendsto line 26
  4. def OAI.WeakPureInfiniteness.inverseWeightVector line 34
  5. lemma OAI.WeakPureInfiniteness.modularWeightedInverse_integrable line 40
  6. lemma OAI.WeakPureInfiniteness.modularWeightedInverse_tendsto line 61