OAI/Analysis/LipschitzHilbert/Trees/SourceReferenceOrdinaryTree.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Ordinary trees in arbitrary reference coordinates. Original angular cells and density tests are kept through the measure-preserving shear.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_reference_ordinary_tree_estimate line 15