OAI/Geometry/Immersion/ClosedSurface/ForcedModes.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ClosedSurfaceR4.RealModes.norm_realPartCLM_le line 13
  2. def OAI.ClosedSurfaceR4.RealModes.realOsc line 20
  3. lemma OAI.ClosedSurfaceR4.RealModes.realOsc_eq_displacement line 23
  4. lemma OAI.ClosedSurfaceR4.RealModes.contDiffOn_realOsc line 33
  5. lemma OAI.ClosedSurfaceR4.RealModes.weighted_realPart line 37
  6. lemma OAI.ClosedSurfaceR4.RealModes.weighted_realOsc line 44
  7. lemma OAI.ClosedSurfaceR4.RealModes.coordDeriv_realPart line 51
  8. lemma OAI.ClosedSurfaceR4.RealModes.complexify_dot_realPart line 57
  9. def OAI.ClosedSurfaceR4.RealModes.realMetric line 62
  10. def OAI.ClosedSurfaceR4.RealModes.realLinearized line 65
  11. lemma OAI.ClosedSurfaceR4.RealModes.realMetric_add line 68
  12. lemma OAI.ClosedSurfaceR4.RealModes.realLinearized_realPart line 78
  13. lemma OAI.ClosedSurfaceR4.RealModes.realLinearized_realOsc line 85
  14. def OAI.ClosedSurfaceR4.RealModes.realMetricTensor line 95
  15. def OAI.ClosedSurfaceR4.RealModes.realLinearizedTensor line 98
  16. lemma OAI.ClosedSurfaceR4.RealModes.realLinearized_residual line 102
  17. theorem OAI.ClosedSurfaceR4.RealModes.real_finite_forced_mode line 114
  18. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.enlarge_scale line 157