OAI/Analysis/LipschitzHilbert/Trees/SourceGoodPathSet.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The source good set controls the pointwise total bad-top mass. Its measure estimate follows from the full weighted bad-path integral.

  1. def OAI.LipschitzHilbert.sourceBadPathMass line 16
  2. def OAI.LipschitzHilbert.sourceGoodPathSet line 19
  3. theorem OAI.LipschitzHilbert.sourceBadPathMass_eq_filter line 24
  4. theorem OAI.LipschitzHilbert.source_good_path_set_area line 29