OAI/Analysis/LipschitzHilbert/Trees/SourceAssignedParentCentralGain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The original-packet central gain with one numerical threshold chosen before the finite types and packet family. The fixed-family theorem is retained separately; the proof uses the type-uniform moment chain.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.eventually_assigned_parent_central_gain line 15