OAI/Analysis/LipschitzHilbert/Trees/SourcePhysicalAmplitudeMotion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Predictable motion for the original physical coefficients, original length stopping, actual top masks, and actual angular masses.

  1. theorem OAI.LipschitzHilbert.AngularGrid.source_physical_amplitude_motion line 16