OAI/Analysis/RieszRectifiability/Flatness/FlatSeedGlobalCharge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Charging nonflat descendants below a flat seed

The propagation horizon and positive flatness threshold are chosen uniformly before the measure. A descendant with large bilateral beta below a flat seed then yields a bad oscillation cell at an intermediate depth. Composition of relative descendants places this witness in the original cell tree, preserving containment between the nonflat descendant, its charged bad cell, and the flat seed.

  1. theorem OAI.RieszRectifiability.exists_uniform_flat_seed_global_charge line 24