OAI/Geometry/Immersion/ClosedSurface/QuadraticMean.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ClosedSurfaceR4.QuadraticMean.Base line 13
  2. abbrev OAI.ClosedSurfaceR4.QuadraticMean.CVec line 14
  3. abbrev OAI.ClosedSurfaceR4.QuadraticMean.RVec line 15
  4. def OAI.ClosedSurfaceR4.QuadraticMean.realPart line 17
  5. def OAI.ClosedSurfaceR4.QuadraticMean.conjugate line 19
  6. def OAI.ClosedSurfaceR4.QuadraticMean.phase line 21
  7. def OAI.ClosedSurfaceR4.QuadraticMean.realMode line 23
  8. lemma OAI.ClosedSurfaceR4.QuadraticMean.phase_add line 25
  9. lemma OAI.ClosedSurfaceR4.QuadraticMean.phase_conj line 28
  10. lemma OAI.ClosedSurfaceR4.QuadraticMean.phase_sub line 33
  11. lemma OAI.ClosedSurfaceR4.QuadraticMean.phase_zero line 36
  12. lemma OAI.ClosedSurfaceR4.QuadraticMean.real_product line 38
  13. lemma OAI.ClosedSurfaceR4.QuadraticMean.mode_product line 42
  14. theorem OAI.ClosedSurfaceR4.QuadraticMean.realMode_dot line 51
  15. theorem OAI.ClosedSurfaceR4.QuadraticMean.realMode_self_phase line 62
  16. def OAI.ClosedSurfaceR4.QuadraticMean.derivativeAmplitude line 71
  17. def OAI.ClosedSurfaceR4.QuadraticMean.displacement line 76
  18. def OAI.ClosedSurfaceR4.QuadraticMean.realPartCLM line 79
  19. lemma OAI.ClosedSurfaceR4.QuadraticMean.realPartCLM_apply line 82
  20. lemma OAI.ClosedSurfaceR4.QuadraticMean.phase_comp_hasFDerivAt line 84
  21. lemma OAI.ClosedSurfaceR4.QuadraticMean.derivative_displacement line 96
  22. def OAI.ClosedSurfaceR4.QuadraticMean.zeroPair line 116
  23. def OAI.ClosedSurfaceR4.QuadraticMean.doublePair line 118
  24. def OAI.ClosedSurfaceR4.QuadraticMean.crossPair line 121
  25. theorem OAI.ClosedSurfaceR4.QuadraticMean.finite_phase_expansion line 128
  26. lemma OAI.ClosedSurfaceR4.QuadraticMean.differentiableAt_displacement line 144
  27. def OAI.ClosedSurfaceR4.QuadraticMean.sumDisplacement line 150
  28. def OAI.ClosedSurfaceR4.QuadraticMean.quadraticMetric line 154
  29. def OAI.ClosedSurfaceR4.QuadraticMean.meanMetric line 157
  30. theorem OAI.ClosedSurfaceR4.QuadraticMean.quadraticMetric_expansion line 164
  31. def OAI.ClosedSurfaceR4.QuadraticMean.leadingAmplitude line 183
  32. lemma OAI.ClosedSurfaceR4.QuadraticMean.leadingAmplitude_zeroPair line 186