TreeTerminal.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Total displacement of the actual finite tree at the terminal sequence

The displacement through depth N is terminalDefect (N+1). The transmitted-subtree estimate only needs the internal part through depth N-1. Both are finite sums of actual generated-map displacements.

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.terminalDefect_nonneg line 26
theorem OAI.ReflexiveFixedPoints.TreeEvaluation.terminalDefect_le_succ line 33
Source documentation
Including the terminal level can only increase total displacement.
```
theorem terminalDefect_le_succ {X : Type*}
    [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
    {T : OrderedTree} {W : WeightedTree T} {K : Set X}
    (E : TreeEvaluation W K) (N : ℕ) (b : K) :
    E.terminalDefect N b ≤ E.terminalDefect (N + 1) b := by
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedTree, OAI.ReflexiveFixedPoints.WeightedTree, OAI.ReflexiveFixedPoints.TreeEvaluation

theorem OAI.ReflexiveFixedPoints.TreeEvaluation.terminalDefect_terminalSequence_tendsto line 43

Source documentation

The total displacement of every fixed finite actual tree tends to zero on its one common resolvent terminal sequence.

theorem terminalDefect_terminalSequence_tendsto
    (hKclosed : IsClosed K) (hKconvex : Convex ℝ K)
    (F : K → K) (hF : LipschitzWith 1 F)
    (hdiam : ∀ a b : K, ‖(a : X) - b‖ ≤ 1)
    (hgenerated : ∀ k v, Generated hKclosed hKconvex F hF (E.map k v))
    (x : K) (N : ℕ) :
    Tendsto (fun j => E.terminalDefect N (terminalSequence hKclosed hKconvex F hF x j))
      atTop (𝓝 0) := by
…

Mentions: OAI.ReflexiveFixedPoints.Generated, OAI.ReflexiveFixedPoints.terminalSequence