OAI/Geometry/PrescribedRicci/CalabiCutoffCalculus.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Calabi Cutoff Calculus.

  1. def OAI.Anticanonical.SourceSmooth.KaehlerMetric.localLap line 20
  2. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.localLap_affine line 23
  3. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.localLap_abs_bound line 33
  4. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.gradientPair_norm_bound line 42
  5. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.holRealDeriv_square line 59
  6. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.norm_pi_sq_bound line 67
  7. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.square_absorb line 73
  8. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.cutoff_cross_bound line 77