OAI/Analysis/RieszRectifiability/Limits/CappedWeakConvergence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Weak convergence of capped pair energies

Bounded continuous tests pass to weak limits of finite measures. Finite measurable partitions with shrinking cells then control bounded Lipschitz tests on product measures. The capped pair energy of a bounded Lipschitz function satisfies these test bounds, giving convergence of its double integral at each positive cap.

  1. theorem OAI.RieszRectifiability.bounded_continuous_integral_tendsto line 23
  2. theorem OAI.RieszRectifiability.bounded_lipschitz_product_integral_tendsto line 38
  3. theorem OAI.RieszRectifiability.cappedPairEnergy_bounded_lipschitz line 72
  4. theorem OAI.RieszRectifiability.capped_energy_tendsto_of_weak line 106