OAI/Analysis/LipschitzHilbert/Phase/AngularSegmentWeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact exponential form of a source path product beginning at an arbitrary angular level. This connects the shared family with the full-root-paid segment variation estimate.

  1. theorem OAI.LipschitzHilbert.segmentWeight_eq_path_product line 14