OAI/Analysis/LipschitzHilbert/Estimates/TopCovariantData.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A second raw covariant wave supplies the neighborhood estimate for the first covariant derivative, while the analyzing coefficients stay fixed.

  1. structure OAI.LipschitzHilbert.TopCovariantData line 12
  2. theorem OAI.LipschitzHilbert.planarPacketInterval_scaled_covariant_eq line 34