OAI/MeasureTheory/FalconerCompletion/Shells/TransportedAngularField.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Dyadic shells and prefix decompositions.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.transportedAngularField line 26
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.angularWord_pull_exact line 30
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.normalizedAngularWord_pull_exact line 54
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixEndpoint_word_exact line 70
  5. abbrev OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PrefixAssignment line 106
  6. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.prefixLeftWords line 109
  7. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.prefixRightWords line 112
  8. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixInverseLeft line 119
  9. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixInverseRight line 124
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixInverseLeft_eq line 130
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixInverseRight_eq line 141
  12. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixInverseLeft_measurable line 152
  13. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixInverseRight_measurable line 158
  14. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixInverseWord_total line 164
  15. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_prefixInverse_support line 173
  16. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.prefixInverseVocabulary line 215
  17. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.prefixInverseVocabulary_budget line 223
  18. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.prefixInverseVocabulary_mem line 234
  19. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_prefixInverse_derivatives line 245