OAI/MeasureTheory/FalconerCompletion/Shells/PrefixSpatialLeft.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Dyadic shells and prefix decompositions.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixSpatialLeft line 25
  2. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixSpatialRight line 29
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixSpatialLeft_measurable line 34
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixSpatialRight_measurable line 38
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixSpatial_global_bound line 43
  6. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixAngularCorrelation line 58
  7. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixAngularHF line 64
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixAngularCorrelation_measurable line 70
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixAngularHF_integrable line 75
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixAngularHF_nonneg line 86
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixAngularHF_global_bound line 112
  12. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixInverseHF_finite_family line 139
  13. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.bounded_angular_cauchy line 174
  14. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixAngularH line 218
  15. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixAngularHF_le_H line 224