OAI/Geometry/SurfaceImmersion/Correction/QuadratureMean.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Recover the zero Fourier mode from two quadrature displacements.

  1. lemma OAI.ClosedSurfaceR4.QuadraticMean.conjugate_I_smul line 11
  2. lemma OAI.ClosedSurfaceR4.QuadraticMean.zeroPair_quadrature line 16
  3. lemma OAI.ClosedSurfaceR4.QuadraticMean.derivativeAmplitude_const_smul line 29
  4. lemma OAI.ClosedSurfaceR4.RealModes.phaseZeroTensor_quadrature line 44