OAI/Analysis/RieszRectifiability/Limits/CompactWeakConvergence.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RieszRectifiability.CompactTestConvergence line 13
2. def OAI.RieszRectifiability.compactWeightedFiniteMeasure line 17
3. theorem OAI.RieszRectifiability.compactWeightedFiniteMeasure_integral line 26
4. theorem OAI.RieszRectifiability.compactWeightedFiniteMeasure_tendsto line 32
5. theorem OAI.RieszRectifiability.exists_compact_nonneg_cutoff line 49
6. theorem OAI.RieszRectifiability.compactWeightedFiniteMeasure_restrict line 63
7. theorem OAI.RieszRectifiability.relativelyCompact_restrict_finite line 76
8. def OAI.RieszRectifiability.relativelyCompactFiniteMeasure line 81
9. theorem OAI.RieszRectifiability.compactTestConvergence_restrict_tendsto line 85