OAI/MeasureTheory/FalconerCompletion/Angular/AssemblyEndpointNormLe.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Angular cutoffs and derivative estimates.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyEndpoint_norm_le line 24
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_assemblyEndpoint_derivatives line 29
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyEndpoint_word_exact line 41
  4. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyInverseLeft line 60
  5. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyInverseRight line 65
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyInverseLeft_eq line 71
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyInverseRight_eq line 83
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyInverseLeft_measurable line 95
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyInverseRight_measurable line 104
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyInverse_bounds line 114
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyInverse_total line 132
  12. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblySpatialFactor line 151
  13. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblySpatialFactor_measurable line 154
  14. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblySpatialFactor_norm line 160
  15. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assembly_left_transform line 167
  16. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assembly_right_transform line 191
  17. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assembly_HF_transform line 215
  18. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assembly_bounded_cutoff line 243
  19. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assembly_cutoff_transfer line 266