OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The horizontal interval derivative bound for the original labeled source collection. Actual physical analyzing coefficients are retained; the fixed number of lattice slots costs one power of the large parameter.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.planarPacketInterval_horizontal_differentiable_schwartz line 16
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.lattice_rawInterval_horizontal_differentiable line 33
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.source_labeled_top_derivative line 41