OAI/Analysis/RieszRectifiability/Flatness/FlatSeedChainPropagation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Propagation from a flat seed

A thin support tube supplies the initial excess bounds for a dyadic chain. Uniformly small scalar oscillation propagates those bounds and bilateral flatness to its descendants. Conversely, a bad descendant scale provides a mean-zero Lipschitz test with a large scalar Riesz pairing at an earlier scale. The propagation parameters are chosen before the measure and the seed ball.

  1. theorem OAI.RieszRectifiability.exists_uniform_flat_seed_chain_propagation line 23
  2. theorem OAI.RieszRectifiability.exists_uniform_flat_seed_bad_scale_witness line 55