Documentation

ConNF.FOA.StrApprox

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 [Params] :

TypeIndex → Type u

Equations

ConNF.StrApprox = ConNF.Tree ConNF.BaseApprox

Instances For

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

Equations

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

Instances For

theorem ConNF.StrApprox.addOrbit_apply [Params] {β : TypeIndex} {ψ : StrApprox β} {A : β ↝ ⊥} {f : ℤ → 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 [Params] {β : TypeIndex} {ψ : StrApprox β} {A : β ↝ ⊥} {f : ℤ → 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 [Params] {β : TypeIndex} {ψ : StrApprox β} {A : β ↝ ⊥} {f : ℤ → 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 [Params] {β : TypeIndex} (c : Set (StrApprox β)) (hc : IsChain (fun (x1 x2 : StrApprox β) => x1 ≤ x2) c) :

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) ⋯

Instances For

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

ψ ∈ c → ψ ≤ upperBound c hc

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

(upperBound c hc A).exceptions a₁ a₂ ↔ ∃ ψ ∈ c, (ψ A).exceptions a₁ a₂

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

(upperBound c hc A)ᴸ L₁ L₂ ↔ ∃ ψ ∈ c, (ψ A)ᴸ L₁ L₂

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

(upperBound c hc A).typical a₁ a₂ ↔ ∃ ψ ∈ c, (ψ A).typical a₁ a₂

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

(upperBound c hc A)ᴬ a₁ a₂ ↔ ∃ ψ ∈ c, (ψ A)ᴬ a₁ a₂

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

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

Equations

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

Instances For

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

Total (ψ ⇘ A)

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

χ • S = π • S

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

CoherentAt χ A L₁ L₂

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

Equations

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

Instances For

theorem ConNF.StrApprox.addOrbit_coherent [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] {ψ : StrApprox β} {A : β ↝ ⊥} {f : ℤ → 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 : ℤ), CoherentAt ψ A (f n) (f (n + 1))) :

(ψ.addOrbit A f hf hfψ).Coherent

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

Coherent (ψ ⇘ A)

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

(upperBound c hc₁).Coherent

theorem ConNF.StrApprox.exists_maximal_coherent [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (ψ : StrApprox β) (hψ : ψ.Coherent) :

∃ χ ≥ ψ, Maximal {χ : StrApprox β | χ.Coherent} χ