OAI/Geometry/Immersion/ClosedSurface/PhaseMean.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ClosedSurfaceR4.PhaseMean.Tensor line 18
  2. def OAI.ClosedSurfaceR4.PhaseMean.firstDirection line 20
  3. def OAI.ClosedSurfaceR4.PhaseMean.secondDirection line 21
  4. lemma OAI.ClosedSurfaceR4.PhaseMean.firstDirection_norm line 23
  5. lemma OAI.ClosedSurfaceR4.PhaseMean.secondDirection_norm line 25
  6. def OAI.ClosedSurfaceR4.PhaseMean.evaluate line 28
  7. def OAI.ClosedSurfaceR4.PhaseMean.pullback line 32
  8. def OAI.ClosedSurfaceR4.PhaseMean.pullbackField line 38
  9. def OAI.ClosedSurfaceR4.PhaseMean.meanTensor line 42
  10. lemma OAI.ClosedSurfaceR4.PhaseMean.contDiffOn_meanTensor line 45
  11. lemma OAI.ClosedSurfaceR4.PhaseMean.weighted_meanTensor line 54
  12. lemma OAI.ClosedSurfaceR4.PhaseMean.weighted_meanTensor_difference line 72
  13. def OAI.ClosedSurfaceR4.PhaseMean.coefficient line 97
  14. def OAI.ClosedSurfaceR4.PhaseMean.meanTerm line 102
  15. lemma OAI.ClosedSurfaceR4.PhaseMean.contDiffOn_coefficient line 115
  16. lemma OAI.ClosedSurfaceR4.PhaseMean.weighted_coefficient line 121
  17. lemma OAI.ClosedSurfaceR4.PhaseMean.weighted_coefficient_difference line 135
  18. lemma OAI.ClosedSurfaceR4.PhaseMean.coefficient_trial_range line 151