OAI/Geometry/PrescribedRicci/HolderFiniteProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Holder Finite Product.

  1. lemma OAI.TameInterpolation.lpNorm_finite_prod line 18
  2. lemma OAI.TameInterpolation.exponent_sum_inverse line 36