OAI/Analysis/LipschitzHilbert/Trees/SourceOrdinaryModelConfig.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fixed geometric and selector data for the ordinary model. None of these parameters depends on the input function or the tested set.

  1. structure OAI.LipschitzHilbert.SourceLabeledLattice.OrdinaryModelConfig line 15
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.ordinaryTreeConstant_nonneg line 88
  3. def OAI.LipschitzHilbert.SourceLabeledLattice.OrdinaryModelConfig.sizeAreaConstant line 99
  4. def OAI.LipschitzHilbert.SourceLabeledLattice.OrdinaryModelConfig.stepConstant line 103
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.OrdinaryModelConfig.sizeAreaConstant_nonneg line 107
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.OrdinaryModelConfig.stepConstant_nonneg line 112