OAI/Analysis/RieszRectifiability/Limits/WeakRestriction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Weak convergence on continuity sets

Weak convergence of finite measures controls the masses of sets with null boundary. Weighting by bounded continuous nonnegative functions transfers this control to restricted integrals, providing continuity-set versions of the weak convergence estimates.

  1. theorem OAI.RieszRectifiability.finiteMeasure_continuitySet_mass_tendsto line 22
  2. def OAI.RieszRectifiability.weightedFiniteMeasure line 36
  3. theorem OAI.RieszRectifiability.weightedFiniteMeasure_integral line 41
  4. theorem OAI.RieszRectifiability.weightedFiniteMeasure_real_set line 48
  5. theorem OAI.RieszRectifiability.weightedFiniteMeasure_tendsto line 56
  6. theorem OAI.RieszRectifiability.weak_setIntegral_nnreal_tendsto line 67
  7. theorem OAI.RieszRectifiability.weak_setIntegral_tendsto line 79
  8. def OAI.RieszRectifiability.restrictedFiniteMeasure line 89
  9. theorem OAI.RieszRectifiability.restrictedFiniteMeasure_tendsto line 92