OAI/Analysis/LipschitzHilbert/Trees/SourceSelectedGoodPathArea.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Selected residual packet families have event-dependent spatial item fibers. The weighted good-path argument only uses their measurable physical bad events, so the exact same area estimate applies without identifying these different finite item types.

  1. theorem OAI.LipschitzHilbert.eventually_selected_physical_reference_good_path_area line 15