OAI/Analysis/LipschitzHilbert/Trees/SourceScaledTopGood.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Top concentration at the actual horizontal frequency scale. Each top is normalized separately; its exceptional area is transported back before forming the common exceptional set.

  1. theorem OAI.LipschitzHilbert.PlanarPacketFamily.source_scaled_top_good line 15