OAI/Analysis/LipschitzHilbert/Packets/PacketDataSupportedAssignedConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Original-selector concentration for the assigned top families, recentered at their own slopes. All source bounds concern the original labels and selected packets. Neither restriction introduces multiplicity or changes the analyzing coefficient.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.eventually_assigned_top_selector_concentration_of_supported line 17