Flexible approximations

In this file, we define flexible approximations.

Main declarations

• ConNF.FlexApprox: Flexible approximations.

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

TODO: Fix definition in blueprint to this.

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

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

theorem ConNF.BaseAction.smul_nearLitter_of_smul_litter [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ξ : ConNF.BaseAction} {ψ : ConNF.BaseApprox} {A : β ↝ ⊥} {π : ConNF.BasePerm} {N₁ N₂ : ConNF.NearLitter} (hξ : ConNF.BaseAction.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 [ConNF.Params] {ξ : ConNF.BaseAction} : Cardinal.mk ↑(ξᴸ.dom ∪ ξᴸ.codom)ᶜ = Cardinal.mk ConNF.μ

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

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

Equations

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

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

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

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

Equations

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

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

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

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

TODO: Move this to PermutativeExtension and do it abstractly.

Equations

• ξ.litterPerm = ξ.littersExtension.toEquiv ⋯

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

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

Equations

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

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

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

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

Equations

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

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

Equations

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

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

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

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

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

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

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

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

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

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

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

Equations

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

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

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

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

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

Equations

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

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

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

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

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

Equations

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

def ConNF.BaseAction.MapFlexible [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (ξ : ConNF.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' [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ξ : ConNF.BaseAction} {A : β ↝ ⊥} (hξ₁ : ξ.MapFlexible A) (hξ₂ : ξ.Nice) : ConNF.BaseAction.FlexApprox A ξ (ξ.flexApprox' A)

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

A flexible approximation for ξ along A.

Equations

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

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

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