OAI/Analysis/LipschitzHilbert/Estimates/IntegralMinkowski.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite Minkowski inequality in the integral form needed by the diagonal Hilbert extension.

  1. theorem OAI.LipschitzHilbert.PhaseCombinatorics.lpNorm_nonnegative_eq line 16
  2. theorem OAI.LipschitzHilbert.PhaseCombinatorics.integral_finite_minkowski line 23