OAI/MeasureTheory/FalconerCompletion/Shells/PrefixParallelMem.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Dyadic shells and prefix decompositions.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.source_prefix_parallel_mem line 27
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.prefix_high_graph_ranges line 42
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixInverseLeft_contDiff line 64
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixInverseRight_contDiff line 74
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixPhasedLeft_measurable line 84
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixPhasedRight_measurable line 90
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixPhased_jets line 96
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixAngularHF_graph_eq line 118
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefix_graph_centers line 137
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_prefixPhased_imposes line 149
  11. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_actual_prefix_inverse_graph line 208
  12. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixHighChildValues line 345
  13. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.prefixHighChildSup line 349