OAI/Geometry/PrescribedRicci/InterpolationExponents.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Interpolation Exponents.

  1. def OAI.TameInterpolation.exponent line 11
  2. lemma OAI.TameInterpolation.exponent_zero line 13
  3. lemma OAI.TameInterpolation.exponent_of_pos line 15
  4. lemma OAI.TameInterpolation.holder_inverse line 23
  5. lemma OAI.TameInterpolation.exponent_middle_gt line 28
  6. lemma OAI.TameInterpolation.exponent_holder_step line 34
  7. lemma OAI.TameInterpolation.interpolation_holder_conjugate line 46
  8. lemma OAI.TameInterpolation.interpolation_power_exponent line 53