OAI/Analysis/LipschitzHilbert/Trees/SourceAssignedParentCentralInputs.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual concentration and reference good set supplies every local input used by central interpolation: the original node bounds, weighted bad-path budget and common-count original vertex integrals. No moment, path-product or plane estimate is assumed.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.eventually_assigned_parent_central_inputs line 19