OAI/Analysis/LipschitzHilbert/Packets/PacketDataAssignedParentCentralGain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The original-packet central gain has one numerical threshold chosen before the finite types and packet family. Its estimate follows from the type-uniform moment bounds.

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