OAI/Geometry/PrescribedRicci/ComplexJetProduct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Complex Jet Product.

  1. lemma OAI.TameInterpolation.lpNorm_complex_mul_le line 18
  2. lemma OAI.TameInterpolation.lpNorm_complex_finite_prod line 27
  3. lemma OAI.TameInterpolation.exponent_one_le line 45
  4. theorem OAI.TameInterpolation.cjet_product_L2 line 59