Fixed points of maps that compute each coordinate from those below it

Let r be a well-founded relation on an index type ι, and let F : (∀ i, β i) → ∀ i, β i be a map whose i-th coordinate depends only on the coordinates r-below i, that is DependsOn (F · i) {j | r j i}. This file proves that F has exactly one fixed point, WellFounded.fixedPoint, built by well-founded recursion, and that iterating F from any family reaches it once the number of iterations exceeds a ranking of r, which in a finite index type is its cardinality. Fixed points of two such maps compare when the maps do.

Main definitions

• WellFounded.fixedPoint: the fixed point of a map computing each coordinate from those below

Main results

• WellFounded.isFixedPt_fixedPoint, WellFounded.eq_fixedPoint_of_isFixedPt: it is the unique fixed point
• WellFounded.fixedPoint_eq_iterate, WellFounded.fixedPoint_eq_iterate_card: iteration reaches it past a ranking
• WellFounded.fixedPoint_le_fixedPoint: fixed points are ordered as the maps are

theorem WellFounded.iterate_apply_eq_of_dependsOn {ι : Type u_1} {β : ι → Type u_2} {r : ι → ι → Prop} {F : ((i : ι) → β i) → (i : ι) → β i} (hF : ∀ (i : ι), DependsOn (fun (x : (i : ι) → β i) => F x i) {j : ι | r j i}) (rk : r →r fun (x1 x2 : ℕ) => x1 < x2) {k : ℕ} {i : ι} (hi : rk i < k) (x y : (i : ι) → β i) : F^[k] x i = F^[k] y i

After k rounds of F, a coordinate ranked below k no longer depends on the family the rounds started from.

noncomputable def WellFounded.fixedPoint {ι : Type u_1} {β : ι → Type u_2} {r : ι → ι → Prop} [∀ (i : ι), Nonempty (β i)] (hr : WellFounded r) (F : ((i : ι) → β i) → (i : ι) → β i) (i : ι) : β i

The fixed point of a map computing each coordinate from those r-below it, by well-founded recursion. Coordinates not below the current one are filled arbitrarily, which the map ignores.

Equations

• hr.fixedPoint F = hr.fix fun (i : ι) (rec : (y : ι) → r y i → β y) => F (fun (j : ι) => if h : r j i then rec j h else Classical.arbitrary (β j)) i

theorem WellFounded.isFixedPt_fixedPoint {ι : Type u_1} {β : ι → Type u_2} {r : ι → ι → Prop} {F : ((i : ι) → β i) → (i : ι) → β i} [∀ (i : ι), Nonempty (β i)] (hr : WellFounded r) (hF : ∀ (i : ι), DependsOn (fun (x : (i : ι) → β i) => F x i) {j : ι | r j i}) : Function.IsFixedPt F (hr.fixedPoint F)

theorem WellFounded.eq_fixedPoint_of_isFixedPt {ι : Type u_1} {β : ι → Type u_2} {r : ι → ι → Prop} {F : ((i : ι) → β i) → (i : ι) → β i} [∀ (i : ι), Nonempty (β i)] {hr : WellFounded r} (hF : ∀ (i : ι), DependsOn (fun (x : (i : ι) → β i) => F x i) {j : ι | r j i}) {x : (i : ι) → β i} (hx : Function.IsFixedPt F x) : x = hr.fixedPoint F

theorem WellFounded.isFixedPt_iff_eq_fixedPoint {ι : Type u_1} {β : ι → Type u_2} {r : ι → ι → Prop} {F : ((i : ι) → β i) → (i : ι) → β i} [∀ (i : ι), Nonempty (β i)] {hr : WellFounded r} (hF : ∀ (i : ι), DependsOn (fun (x : (i : ι) → β i) => F x i) {j : ι | r j i}) {x : (i : ι) → β i} : Function.IsFixedPt F x ↔ x = hr.fixedPoint F

theorem WellFounded.fixedPoint_apply {ι : Type u_1} {β : ι → Type u_2} {r : ι → ι → Prop} {F : ((i : ι) → β i) → (i : ι) → β i} [∀ (i : ι), Nonempty (β i)] {hr : WellFounded r} (hF : ∀ (i : ι), DependsOn (fun (x : (i : ι) → β i) => F x i) {j : ι | r j i}) (i : ι) : hr.fixedPoint F i = F (hr.fixedPoint F) i

theorem WellFounded.fixedPoint_eq_iterate {ι : Type u_1} {β : ι → Type u_2} {r : ι → ι → Prop} {F : ((i : ι) → β i) → (i : ι) → β i} [∀ (i : ι), Nonempty (β i)] {hr : WellFounded r} (hF : ∀ (i : ι), DependsOn (fun (x : (i : ι) → β i) => F x i) {j : ι | r j i}) (rk : r →r fun (x1 x2 : ℕ) => x1 < x2) {n : ℕ} (hn : ∀ (i : ι), rk i < n) (x : (i : ι) → β i) : hr.fixedPoint F = F^[n] x

Iterating from any family past a ranking of r reaches the fixed point.

theorem WellFounded.exists_relHom_lt_card {ι : Type u_1} {r : ι → ι → Prop} [Fintype ι] (hr : WellFounded r) : ∃ (rk : r →r fun (x1 x2 : ℕ) => x1 < x2), ∀ (i : ι), rk i < Fintype.card ι

On a finite index type, counting strict predecessors ranks a well-founded relation below the number of indices.

theorem WellFounded.fixedPoint_eq_iterate_card {ι : Type u_1} {β : ι → Type u_2} {r : ι → ι → Prop} {F : ((i : ι) → β i) → (i : ι) → β i} [∀ (i : ι), Nonempty (β i)] {hr : WellFounded r} (hF : ∀ (i : ι), DependsOn (fun (x : (i : ι) → β i) => F x i) {j : ι | r j i}) [Fintype ι] (x : (i : ι) → β i) : hr.fixedPoint F = F^[Fintype.card ι] x

On a finite index type, iterating once per index reaches the fixed point.

theorem WellFounded.fixedPoint_le_fixedPoint {ι : Type u_1} {β : ι → Type u_2} {r : ι → ι → Prop} {F G : ((i : ι) → β i) → (i : ι) → β i} [∀ (i : ι), Nonempty (β i)] {hr : WellFounded r} [(i : ι) → Preorder (β i)] (hF : ∀ (i : ι), DependsOn (fun (x : (i : ι) → β i) => F x i) {j : ι | r j i}) (hG : ∀ (i : ι), DependsOn (fun (x : (i : ι) → β i) => G x i) {j : ι | r j i}) (hFG : ∀ (x y : (i : ι) → β i), x ≤ y → F x ≤ G y) : hr.fixedPoint F ≤ hr.fixedPoint G

Fixed points are ordered as the maps are. If F x ≤ G y whenever x ≤ y, the fixed point of F lies below that of G.