Flexible approximations

In this file, we define flexible approximations.

Main declarations

• ConNF.FlexApprox: Flexible approximations.

structure ConNF.BaseAction.FlexApprox [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (A : β ↝ ⊥) (ξ : BaseAction) (ψ : BaseApprox) : Prop

TODO: Fix definition in blueprint to this.

• atoms_le_atoms : ξᴬ ≤ ψ.exceptions
• flexible_of_mem_dom {L : Litter} : L ∈ ψᴸ.dom → ¬Inflexible A L
• litters_of_flexible {L₁ L₂ : Litter} : ¬Inflexible A L₁ → ξᴸ L₁ L₂ → ψᴸ L₁ L₂
• symmDiff_subset_dom {N : NearLitter} : N ∈ ξᴺ.dom → symmDiff Nᴬ Nᴸᴬ ⊆ ψ.exceptions.dom
• symmDiff_subset_codom {N : NearLitter} : N ∈ ξᴺ.codom → symmDiff Nᴬ Nᴸᴬ ⊆ ψ.exceptions.codom
• mem_iff_mem {N₁ N₂ : NearLitter} : ξᴺ N₁ N₂ → ∀ (a₂ : Atom), a₂ ∈ N₂ᴬ ↔ (∃ a₁ ∈ N₁ᴬ, ψ.exceptions a₁ a₂) ∨ a₂ ∉ ψ.exceptions.dom ∧ a₂ᴸ = N₂ᴸ

theorem ConNF.BaseAction.FlexApprox.mono [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {A : β ↝ ⊥} {ξ ζ : BaseAction} {ψ : BaseApprox} (hξ : FlexApprox A ξ ψ) (h : ζ ≤ ξ) : FlexApprox A ζ ψ

theorem ConNF.BaseAction.smul_nearLitter_of_smul_litter [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {ξ : BaseAction} {ψ : BaseApprox} {A : β ↝ ⊥} {π : BasePerm} {N₁ N₂ : NearLitter} (hξ : FlexApprox A ξ ψ) (hψ : ψ.ExactlyApproximates π) (hNξ : ξᴺ N₁ N₂) (hNπ : π • N₁ᴸ = N₂ᴸ) : π • N₁ = N₂

The main lemma about how approximations interact with actions.

theorem ConNF.BaseAction.card_litter_dom_compl [Params] {ξ : BaseAction} : Cardinal.mk ↑(ξᴸ.dom ∪ ξᴸ.codom)ᶜ = Cardinal.mk μ

theorem ConNF.BaseAction.litter_dom_compl_infinite [Params] {ξ : BaseAction} : (ξᴸ.dom ∪ ξᴸ.codom)ᶜ.Infinite

def ConNF.BaseAction.littersExtension' [Params] (ξ : BaseAction) : Rel Litter Litter

Equations

• ξ.littersExtension' = ξᴸ.permutativeExtension' ⋯ (ξᴸ.dom ∪ ξᴸ.codom)ᶜ ⋯ ⋯ ⋯

theorem ConNF.BaseAction.le_littersExtension' [Params] (ξ : BaseAction) : ξᴸ ≤ ξ.littersExtension'

theorem ConNF.BaseAction.littersExtension'_permutative [Params] (ξ : BaseAction) : ξ.littersExtension'.Permutative

def ConNF.BaseAction.littersExtension [Params] (ξ : BaseAction) : Rel Litter Litter

Equations

• ξ.littersExtension = ξ.littersExtension' ⊔ fun (L₁ L₂ : ConNF.Litter) => L₁ = L₂ ∧ L₁ ∉ ξ.littersExtension'.dom

theorem ConNF.BaseAction.le_littersExtension [Params] (ξ : BaseAction) : ξᴸ ≤ ξ.littersExtension

theorem ConNF.BaseAction.littersExtension_bijective [Params] (ξ : BaseAction) : ξ.littersExtension.Bijective

def ConNF.BaseAction.litterPerm [Params] (ξ : BaseAction) : Equiv.Perm Litter

TODO: Move this to PermutativeExtension and do it abstractly.

Equations

• ξ.litterPerm = ξ.littersExtension.toEquiv ⋯

theorem ConNF.BaseAction.litterPerm_eq [Params] {ξ : BaseAction} {L₁ L₂ : Litter} (h : ξᴸ L₁ L₂) : ξ.litterPerm L₁ = L₂

def ConNF.BaseAction.insideAll [Params] (ξ : BaseAction) : Set Atom

Equations

• ξ.insideAll = {a : ConNF.Atom | ∀ (N : ConNF.NearLitter), N ∈ ξᴺ.dom ∨ N ∈ ξᴺ.codom → Nᴸ = aᴸ → a ∈ Nᴬ}

theorem ConNF.BaseAction.diff_insideAll_small [Params] (ξ : BaseAction) (L : Litter) : Small (Lᴬ \ ξ.insideAll)

theorem ConNF.BaseAction.card_insideAll_inter [Params] (ξ : BaseAction) (L : Litter) : Cardinal.mk ↑(ξ.insideAll \ (ξᴬ.dom ∪ ξᴬ.codom) ∩ Lᴬ) = Cardinal.mk κ

def ConNF.BaseAction.orbitRestriction [Params] (ξ : BaseAction) : Rel.OrbitRestriction (ξᴬ.dom ∪ ξᴬ.codom) Litter

Equations

• ξ.orbitRestriction = { sandbox := ξ.insideAll \ (ξᴬ.dom ∪ ξᴬ.codom), sandbox_disjoint := ⋯, categorise := fun (a : ConNF.Atom) => aᴸ, catPerm := ξ.litterPerm, le_card_categorise := ⋯ }

def ConNF.BaseAction.atomPerm [Params] (ξ : BaseAction) : Rel Atom Atom

Equations

• ξ.atomPerm = ξᴬ.permutativeExtension ξ.orbitRestriction

theorem ConNF.BaseAction.le_atomPerm [Params] (ξ : BaseAction) : ξᴬ ≤ ξ.atomPerm

theorem ConNF.BaseAction.dom_subset_dom_atomPerm [Params] (ξ : BaseAction) : ξᴬ.dom ⊆ ξ.atomPerm.dom

theorem ConNF.BaseAction.codom_subset_codom_atomPerm [Params] (ξ : BaseAction) : ξᴬ.codom ⊆ ξ.atomPerm.codom

theorem ConNF.BaseAction.atomPerm_permutative [Params] (ξ : BaseAction) : ξ.atomPerm.Permutative

theorem ConNF.BaseAction.litter_of_atomPerm [Params] {ξ : BaseAction} {a₁ a₂ : Atom} : ξ.atomPerm a₁ a₂ → ξᴬ a₁ a₂ ∨ a₁ ∉ ξᴬ.dom ∧ a₂ ∉ ξᴬ.codom ∧ a₂ᴸ = ξ.litterPerm a₁ᴸ

theorem ConNF.BaseAction.atomPerm_dom_subset [Params] (ξ : BaseAction) : ξ.atomPerm.dom ⊆ ξᴬ.dom ∪ ξᴬ.codom ∪ ξ.insideAll

theorem ConNF.BaseAction.atomPerm_small [Params] (ξ : BaseAction) : Small ξ.atomPerm.dom

theorem ConNF.BaseAction.atomPerm_mem_iff_mem [Params] {ξ : BaseAction} (hξ : ξ.Nice) {a₁ a₂ : Atom} {N₁ N₂ : NearLitter} (ha : ξ.atomPerm a₁ a₂) (hN : ξᴺ N₁ N₂) : a₁ ∈ N₁ᴬ ↔ a₂ ∈ N₂ᴬ

theorem ConNF.BaseAction.atomPerm_mem_iff [Params] {ξ : BaseAction} (hξ : ξ.Nice) {N₁ N₂ : NearLitter} (hN : ξᴺ N₁ N₂) (a₂ : Atom) : a₂ ∈ N₂ᴬ ↔ (∃ a₁ ∈ N₁ᴬ, ξ.atomPerm a₁ a₂) ∨ a₂ ∉ ξ.atomPerm.dom ∧ a₂ᴸ = N₂ᴸ

def ConNF.BaseAction.flexLitterRel [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (ξ : BaseAction) (A : β ↝ ⊥) : Rel Litter Litter

Equations

• ξ.flexLitterRel A = ξᴸ ⊓ fun (L₁ L₂ : ConNF.Litter) => ¬ConNF.Inflexible A L₁ ∧ ¬ConNF.Inflexible A L₂

theorem ConNF.BaseAction.flexLitterRel_dom_small [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (ξ : BaseAction) (A : β ↝ ⊥) : Small (ξ.flexLitterRel A).dom

theorem ConNF.BaseAction.card_inflexible [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (A : β ↝ ⊥) : Cardinal.mk ↑{L : Litter | ¬Inflexible A L} = Cardinal.mk μ

theorem ConNF.BaseAction.card_inflexible_diff_dom [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (ξ : BaseAction) (A : β ↝ ⊥) : Cardinal.mk ↑({L : Litter | ¬Inflexible A L} \ (ξᴸ.dom ∪ ξᴸ.codom)) = Cardinal.mk μ

def ConNF.BaseAction.flexLitterPerm [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (ξ : BaseAction) (A : β ↝ ⊥) : Rel Litter Litter

Equations

• ξ.flexLitterPerm A = (ξ.flexLitterRel A).permutativeExtension' ⋯ ({L : ConNF.Litter | ¬ConNF.Inflexible A L} \ (ξᴸ.dom ∪ ξᴸ.codom)) ⋯ ⋯ ⋯

theorem ConNF.BaseAction.le_flexLitterPerm [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (ξ : BaseAction) (A : β ↝ ⊥) : ξ.flexLitterRel A ≤ ξ.flexLitterPerm A

theorem ConNF.BaseAction.flexLitterPerm_permutative [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (ξ : BaseAction) (A : β ↝ ⊥) : (ξ.flexLitterPerm A).Permutative

theorem ConNF.BaseAction.dom_flexLitterPerm_subset [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (ξ : BaseAction) (A : β ↝ ⊥) : (ξ.flexLitterPerm A).dom ⊆ {L : Litter | ¬Inflexible A L}

def ConNF.BaseAction.flexApprox' [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (ξ : BaseAction) (A : β ↝ ⊥) : BaseApprox

Equations

• ξ.flexApprox' A = { exceptions := ξ.atomPerm, litters := ξ.flexLitterPerm A, exceptions_permutative := ⋯, litters_permutative' := ⋯, exceptions_small := ⋯ }

def ConNF.BaseAction.MapFlexible [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (ξ : BaseAction) (A : β ↝ ⊥) : Prop

Equations

• ξ.MapFlexible A = ∀ {L₁ L₂ : ConNF.Litter}, ξᴸ L₁ L₂ → (ConNF.Inflexible A L₁ ↔ ConNF.Inflexible A L₂)

theorem ConNF.BaseAction.flexApprox_flexApprox' [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {ξ : BaseAction} {A : β ↝ ⊥} (hξ₁ : ξ.MapFlexible A) (hξ₂ : ξ.Nice) : FlexApprox A ξ (ξ.flexApprox' A)

def ConNF.BaseAction.flexApprox [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (ξ : BaseAction) (A : β ↝ ⊥) : BaseApprox

A flexible approximation for ξ along A.

Equations

• ξ.flexApprox A = ξ.niceExtension.flexApprox' A

theorem ConNF.BaseAction.niceExtension_mapFlexible [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {ξ : BaseAction} {A : β ↝ ⊥} (hξ : ξ.MapFlexible A) : ξ.niceExtension.MapFlexible A

theorem ConNF.BaseAction.flexApprox_flexApprox [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {ξ : BaseAction} {A : β ↝ ⊥} (hξ : ξ.MapFlexible A) : FlexApprox A ξ (ξ.flexApprox A)