OAI/Analysis/DiamondDistortion/IntrinsicTail.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DiamondDistortion.Ancestry.intrinsic_tail line 21
2. theorem OAI.DiamondDistortion.forest_intrinsic_tail line 38

   Source documentation

   Exact intrinsic input for the headline, on the whole finite-forest dual.

   theorem forest_intrinsic_tail {H : Finset ForestNode}
       (hH : Ancestry.Ancestral (A := forestAncestry) (H : Set ForestNode)) {R : ℝ}
   …

   Mentions: OAI.DiamondDistortion.ForestNode, OAI.DiamondDistortion.Ancestry.Ancestral, OAI.DiamondDistortion.forestAncestry

3. theorem OAI.DiamondDistortion.infinite_intrinsic_tail line 48

   Source documentation

   The intrinsic input for the infinite-height coordinate predual is proved even in the ambient dual. Only finite-head center approximation in the graph deduction is restricted to the closed coordinate span.

   theorem infinite_intrinsic_tail {H : Finset (List ℕ)}
       (hH : Ancestry.Ancestral (A := infiniteAncestry) (H : Set (List ℕ))) {R : ℝ}
   …

   Mentions: OAI.DiamondDistortion.Ancestry.Ancestral, OAI.DiamondDistortion.infiniteAncestry