Structural approximations

In this file, we define structural approximations, which are trees of base approximations.

Main declarations

• ConNF.StrApprox: The type of structural approximations.
• ConNF.InflexiblePath: A pair of paths starting at β that describe a particular way to use a fuzz map.
• ConNF.Inflexible: A litter is said to be inflexible along a path if it can be obtained by applying a fuzz map along this path.

@[reducible, inline]

abbrev ConNF.StrApprox [ConNF.Params] : ConNF.TypeIndex → Type u

Equations

• ConNF.StrApprox = ConNF.Tree ConNF.BaseApprox

def ConNF.StrApprox.addOrbit [ConNF.Params] {β : ConNF.TypeIndex} (ψ : ConNF.StrApprox β) (A : β ↝ ⊥) (f : ℤ → ConNF.Litter) (hf : ∀ (m n k : ℤ), f m = f n → f (m + k) = f (n + k)) (hfψ : ∀ (n : ℤ), f n ∉ (ψ A)ᴸ.dom) : ConNF.StrApprox β

Equations

• ψ.addOrbit A f hf hfψ B = if h : A = B then (ψ B).addOrbit f hf ⋯ else ψ B

theorem ConNF.StrApprox.addOrbit_apply [ConNF.Params] {β : ConNF.TypeIndex} {ψ : ConNF.StrApprox β} {A : β ↝ ⊥} {f : ℤ → ConNF.Litter} {hf : ∀ (m n k : ℤ), f m = f n → f (m + k) = f (n + k)} {hfψ : ∀ (n : ℤ), f n ∉ (ψ A)ᴸ.dom} : ψ.addOrbit A f hf hfψ A = (ψ A).addOrbit f hf hfψ

theorem ConNF.StrApprox.addOrbit_apply_ne [ConNF.Params] {β : ConNF.TypeIndex} {ψ : ConNF.StrApprox β} {A : β ↝ ⊥} {f : ℤ → ConNF.Litter} {hf : ∀ (m n k : ℤ), f m = f n → f (m + k) = f (n + k)} {hfψ : ∀ (n : ℤ), f n ∉ (ψ A)ᴸ.dom} (B : β ↝ ⊥) (hB : A ≠ B) : ψ.addOrbit A f hf hfψ B = ψ B

theorem ConNF.StrApprox.le_addOrbit [ConNF.Params] {β : ConNF.TypeIndex} {ψ : ConNF.StrApprox β} {A : β ↝ ⊥} {f : ℤ → ConNF.Litter} {hf : ∀ (m n k : ℤ), f m = f n → f (m + k) = f (n + k)} {hfψ : ∀ (n : ℤ), f n ∉ (ψ A)ᴸ.dom} : ψ ≤ ψ.addOrbit A f hf hfψ

def ConNF.StrApprox.upperBound [ConNF.Params] {β : ConNF.TypeIndex} (c : Set (ConNF.StrApprox β)) (hc : IsChain (fun (x1 x2 : ConNF.StrApprox β) => x1 ≤ x2) c) : ConNF.StrApprox β

An upper bound for a chain of approximations.

Equations

• ConNF.StrApprox.upperBound c hc A = ConNF.BaseApprox.upperBound ((fun (x : ConNF.StrApprox β) => x A) '' c) ⋯

theorem ConNF.StrApprox.le_upperBound [ConNF.Params] {β : ConNF.TypeIndex} (c : Set (ConNF.StrApprox β)) (hc : IsChain (fun (x1 x2 : ConNF.StrApprox β) => x1 ≤ x2) c) (ψ : ConNF.StrApprox β) : ψ ∈ c → ψ ≤ ConNF.StrApprox.upperBound c hc

theorem ConNF.StrApprox.upperBound_exceptions [ConNF.Params] {β : ConNF.TypeIndex} (c : Set (ConNF.StrApprox β)) (hc : IsChain (fun (x1 x2 : ConNF.StrApprox β) => x1 ≤ x2) c) (A : β ↝ ⊥) (a₁ a₂ : ConNF.Atom) : (ConNF.StrApprox.upperBound c hc A).exceptions a₁ a₂ ↔ ∃ ψ ∈ c, (ψ A).exceptions a₁ a₂

theorem ConNF.StrApprox.upperBound_litters [ConNF.Params] {β : ConNF.TypeIndex} (c : Set (ConNF.StrApprox β)) (hc : IsChain (fun (x1 x2 : ConNF.StrApprox β) => x1 ≤ x2) c) (A : β ↝ ⊥) (L₁ L₂ : ConNF.Litter) : (ConNF.StrApprox.upperBound c hc A)ᴸ L₁ L₂ ↔ ∃ ψ ∈ c, (ψ A)ᴸ L₁ L₂

theorem ConNF.StrApprox.upperBound_typical [ConNF.Params] {β : ConNF.TypeIndex} (c : Set (ConNF.StrApprox β)) (hc : IsChain (fun (x1 x2 : ConNF.StrApprox β) => x1 ≤ x2) c) (A : β ↝ ⊥) (a₁ a₂ : ConNF.Atom) : (ConNF.StrApprox.upperBound c hc A).typical a₁ a₂ ↔ ∃ ψ ∈ c, (ψ A).typical a₁ a₂

theorem ConNF.StrApprox.upperBound_atoms [ConNF.Params] {β : ConNF.TypeIndex} (c : Set (ConNF.StrApprox β)) (hc : IsChain (fun (x1 x2 : ConNF.StrApprox β) => x1 ≤ x2) c) (A : β ↝ ⊥) (a₁ a₂ : ConNF.Atom) : (ConNF.StrApprox.upperBound c hc A)ᴬ a₁ a₂ ↔ ∃ ψ ∈ c, (ψ A)ᴬ a₁ a₂

TODO: Many of the previous lemmas are not actually needed!

def ConNF.StrApprox.Total [ConNF.Params] {β : ConNF.TypeIndex} (ψ : ConNF.StrApprox β) : Prop

Equations

• ψ.Total = ∀ (A : β ↝ ⊥), (ψ A).Total

theorem ConNF.StrApprox.Total.deriv [ConNF.Params] {β : ConNF.TypeIndex} {ψ : ConNF.StrApprox β} (hψ : ψ.Total) {γ : ConNF.TypeIndex} (A : β ↝ γ) : ConNF.StrApprox.Total (ψ ⇘ A)

theorem ConNF.StrApprox.smul_support_eq_smul_mono [ConNF.Params] {β : ConNF.TypeIndex} {ξ χ : ConNF.StrApprox β} {S : ConNF.Support β} {π : ConNF.StrPerm β} (hξ : ξ • S = π • S) (hξχ : ξ ≤ χ) : χ • S = π • S

theorem ConNF.StrApprox.coherentAt_mono [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {ψ χ : ConNF.StrApprox β} {A : β ↝ ⊥} {L₁ L₂ : ConNF.Litter} (h : ConNF.CoherentAt ψ A L₁ L₂) (hψχ : ψ ≤ χ) : ConNF.CoherentAt χ A L₁ L₂

def ConNF.StrApprox.Coherent [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (ψ : ConNF.StrApprox β) : Prop

Equations

• ψ.Coherent = ∀ (A : β ↝ ⊥) (L₁ L₂ : ConNF.Litter), (ψ A)ᴸ L₁ L₂ → ConNF.CoherentAt ψ A L₁ L₂

theorem ConNF.StrApprox.addOrbit_coherent [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} {A : β ↝ ⊥} {f : ℤ → ConNF.Litter} {hf : ∀ (m n k : ℤ), f m = f n → f (m + k) = f (n + k)} {hfψ : ∀ (n : ℤ), f n ∉ (ψ A)ᴸ.dom} (hψ : ψ.Coherent) (hfc : ∀ (n : ℤ), ConNF.CoherentAt ψ A (f n) (f (n + 1))) : (ψ.addOrbit A f hf hfψ).Coherent

theorem ConNF.StrApprox.Coherent.deriv [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} (hψ : ψ.Coherent) {γ : ConNF.TypeIndex} [ConNF.LeLevel γ] (A : β ↝ γ) : ConNF.StrApprox.Coherent (ψ ⇘ A)

theorem ConNF.StrApprox.upperBound_coherent [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (c : Set (ConNF.StrApprox β)) (hc₁ : IsChain (fun (x1 x2 : ConNF.StrApprox β) => x1 ≤ x2) c) (hc₂ : ∀ ψ ∈ c, ψ.Coherent) : (ConNF.StrApprox.upperBound c hc₁).Coherent

theorem ConNF.StrApprox.exists_maximal_coherent [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (ψ : ConNF.StrApprox β) (hψ : ψ.Coherent) : ∃ χ ≥ ψ, Maximal {χ : ConNF.StrApprox β | χ.Coherent} χ