OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledErrorFamily.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Dyadic angular errors on translated lattices with bounded local multiplicity of slope labels. The common source is counted before integration.

  1. structure OAI.LipschitzHilbert.LabeledAngularErrorFamily line 14
  2. def OAI.LipschitzHilbert.LabeledAngularErrorFamily.length line 75
  3. def OAI.LipschitzHilbert.LabeledAngularErrorFamily.angleStep line 78
  4. def OAI.LipschitzHilbert.LabeledAngularErrorFamily.coefficient line 81
  5. def OAI.LipschitzHilbert.LabeledAngularErrorFamily.scaleError line 87
  6. def OAI.LipschitzHilbert.LabeledAngularErrorFamily.error line 92
  7. def OAI.LipschitzHilbert.LabeledAngularErrorFamily.sourceAmplitude line 95
  8. theorem OAI.LipschitzHilbert.LabeledAngularErrorFamily.sourceAmplitude_nonneg line 99
  9. def OAI.LipschitzHilbert.LabeledAngularErrorFamily.sources line 107
  10. theorem OAI.LipschitzHilbert.LabeledAngularErrorFamily.scaleError_le line 112
  11. theorem OAI.LipschitzHilbert.LabeledAngularErrorFamily.error_le_majorant line 133
  12. theorem OAI.LipschitzHilbert.LabeledAngularErrorFamily.scaleError_nonneg line 137
  13. theorem OAI.LipschitzHilbert.LabeledAngularErrorFamily.error_nonneg line 142
  14. theorem OAI.LipschitzHilbert.LabeledAngularErrorFamily.error_measurable line 145
  15. theorem OAI.LipschitzHilbert.LabeledAngularErrorFamily.sources_log_budget line 155