OAI/Geometry/TamingCompatibility/DifferentialForms/HermitianCoefficientBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TamingCompatibility.GeometricChart.schwartz_fderiv_bound line 21
  2. lemma OAI.TamingCompatibility.GeometricChart.schwartz_difference_bound line 26
  3. lemma OAI.TamingCompatibility.GeometricChart.hermitianCenterExtension_bounds line 34
  4. lemma OAI.TamingCompatibility.GeometricChart.hermitianCenterExtension_eventually_eq line 46
  5. lemma OAI.TamingCompatibility.GeometricChart.pullback_complexLine line 66
  6. lemma OAI.TamingCompatibility.GeometricHilbert.closedLift_pullback_complexLine line 91
  7. lemma OAI.TamingCompatibility.GeometricHilbert.correctedDdc_pullback_complexLine line 103
  8. lemma OAI.TamingCompatibility.GeometricHilbert.form_complexLine_norm_le line 120
  9. def OAI.TamingCompatibility.RadialPotential.hermitianLogGradientProfile line 139
  10. def OAI.TamingCompatibility.RadialPotential.hermitianSqrtGradientProfile line 141
  11. lemma OAI.TamingCompatibility.RadialPotential.hermitianLogGradient_eq line 144
  12. lemma OAI.TamingCompatibility.RadialPotential.hermitianSqrtGradient_eq line 150
  13. lemma OAI.TamingCompatibility.RadialPotential.hermitianLogGradient_eq_fderiv line 156
  14. lemma OAI.TamingCompatibility.RadialPotential.hermitianSqrtGradient_eq_fderiv line 164
  15. lemma OAI.TamingCompatibility.RadialPotential.hermitianLogGradient_scale line 172
  16. lemma OAI.TamingCompatibility.RadialPotential.hermitianSqrtGradient_scale line 177