OAI/Analysis/LipschitzHilbert/Estimates/TopEnvelopeDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed top weights preserve the pointwise derivative envelopes needed for the unconditional horizontal derivative estimate.

  1. theorem OAI.LipschitzHilbert.topWeight_mul_envelope line 14
  2. theorem OAI.LipschitzHilbert.top_weighted_selected_derivative line 29