OAI/Analysis/LipschitzHilbert/Phase/SourceRootPathInterpolation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual good-path integrals imply the root diagonal moment. The phase count is chosen after L, and the spatial measure is restricted to the common good set throughout analytic interpolation.

  1. theorem OAI.LipschitzHilbert.AngularGrid.eventually_source_root_diagonal_from_paths line 17