OAI/Analysis/LipschitzHilbert/Estimates/UniformPolynomialMoments.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial moments with a constant chosen before the packet dimension and scale count, including for replacement derivative packets.

  1. theorem OAI.LipschitzHilbert.LinePacketFamily.uniform_polynomial_line_moment line 14