Filling in ranges of base litter actions

In ConNF.FOA.LAction.FillAtomOrbits, we showed that actions can be extended to form precise actions, under a certain condition on the range of their atom map. In this file, we show how to extend arbitrary actions to satisfy this hypothesis.

Main declarations

• ConNF.BaseLAction.fillAtomRange: Fills in images of certain atoms so that completion of orbits in ConNF.BaseLAction.fillAtomOrbits is successful.
• ConNF.BaseLAction.fillAtomRange_symmDiff_subset_ran: The technical condition required to prove ConNF.BaseLAction.fillAtomOrbits_precise.

noncomputable def ConNF.BaseLAction.preimageLitter [ConNF.Params] (φ : ConNF.BaseLAction) : ConNF.Litter

Equations

• φ.preimageLitter = ↑⋯.some

theorem ConNF.BaseLAction.preimageLitter_not_banned [ConNF.Params] (φ : ConNF.BaseLAction) : ¬φ.BannedLitter φ.preimageLitter

theorem ConNF.BaseLAction.withoutPreimage_iff [ConNF.Params] (φ : ConNF.BaseLAction) (a : ConNF.Atom) : φ.WithoutPreimage a ↔ (∃ (L : ConNF.Litter) (hL : (φ.litterMap L).Dom), a ∈ ConNF.litterSet ((φ.litterMap L).get hL).fst) ∧ (∀ (L : ConNF.Litter) (hL : (φ.litterMap L).Dom), a ∉ (φ.litterMap L).get hL) ∧ a ∉ φ.atomMap.ran

structure ConNF.BaseLAction.WithoutPreimage [ConNF.Params] (φ : ConNF.BaseLAction) (a : ConNF.Atom) : Prop

An atom is called without preimage if it is not in the range of the approximation, but it is in a litter near some near-litter in the range. Atoms without preimage need to have something map to it, so that the resulting map that we use in the freedom of action theorem actually maps to the correct near-litter.

• mem_map : ∃ (L : ConNF.Litter) (hL : (φ.litterMap L).Dom), a ∈ ConNF.litterSet ((φ.litterMap L).get hL).fst
• not_mem_map : ∀ (L : ConNF.Litter) (hL : (φ.litterMap L).Dom), a ∉ (φ.litterMap L).get hL
• not_mem_ran : a ∉ φ.atomMap.ran

theorem ConNF.BaseLAction.WithoutPreimage.mem_map [ConNF.Params] {φ : ConNF.BaseLAction} {a : ConNF.Atom} (self : φ.WithoutPreimage a) : ∃ (L : ConNF.Litter) (hL : (φ.litterMap L).Dom), a ∈ ConNF.litterSet ((φ.litterMap L).get hL).fst

theorem ConNF.BaseLAction.WithoutPreimage.not_mem_map [ConNF.Params] {φ : ConNF.BaseLAction} {a : ConNF.Atom} (self : φ.WithoutPreimage a) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) : a ∉ (φ.litterMap L).get hL

theorem ConNF.BaseLAction.WithoutPreimage.not_mem_ran [ConNF.Params] {φ : ConNF.BaseLAction} {a : ConNF.Atom} (self : φ.WithoutPreimage a) : a ∉ φ.atomMap.ran

theorem ConNF.BaseLAction.withoutPreimage_small [ConNF.Params] (φ : ConNF.BaseLAction) : ConNF.Small {a : ConNF.Atom | φ.WithoutPreimage a}

def ConNF.BaseLAction.preimageLitterSubset [ConNF.Params] (φ : ConNF.BaseLAction) : Set ConNF.Atom

The subset of the preimage litter that is put in correspondence with the set of atoms without preimage.

Equations

• φ.preimageLitterSubset = ⋯.choose

theorem ConNF.BaseLAction.preimageLitterSubset_spec [ConNF.Params] (φ : ConNF.BaseLAction) : φ.preimageLitterSubset ⊆ ConNF.litterSet φ.preimageLitter ∧ Cardinal.mk ↑φ.preimageLitterSubset = Cardinal.mk ↑{a : ConNF.Atom | φ.WithoutPreimage a}

theorem ConNF.BaseLAction.preimageLitterSubset_subset [ConNF.Params] (φ : ConNF.BaseLAction) : φ.preimageLitterSubset ⊆ ConNF.litterSet φ.preimageLitter

theorem ConNF.BaseLAction.preimageLitterSubset_small [ConNF.Params] (φ : ConNF.BaseLAction) : ConNF.Small φ.preimageLitterSubset

@[irreducible]

noncomputable def ConNF.BaseLAction.preimageLitterEquiv [ConNF.Params] (φ : ConNF.BaseLAction) : ↑φ.preimageLitterSubset ≃ ↑{a : ConNF.Atom | φ.WithoutPreimage a}

Equations

• @ConNF.BaseLAction.preimageLitterEquiv = ConNF.BaseLAction.wrapped✝.1

theorem ConNF.BaseLAction.preimageLitterEquiv_def [ConNF.Params] (φ : ConNF.BaseLAction) : φ.preimageLitterEquiv = ⋯.some

theorem ConNF.BaseLAction.mappedOutside_iff [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) (a : ConNF.Atom) : φ.MappedOutside L hL a ↔ a ∈ (φ.litterMap L).get hL ∧ a ∉ ConNF.litterSet ((φ.litterMap L).get hL).fst ∧ a ∉ φ.atomMap.ran

structure ConNF.BaseLAction.MappedOutside [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) (a : ConNF.Atom) : Prop

The images of atoms in a litter L that were mapped outside the target litter, but were not in the domain.

• mem_map : a ∈ (φ.litterMap L).get hL
• not_mem_map : a ∉ ConNF.litterSet ((φ.litterMap L).get hL).fst
• not_mem_ran : a ∉ φ.atomMap.ran

theorem ConNF.BaseLAction.MappedOutside.mem_map [ConNF.Params] {φ : ConNF.BaseLAction} {L : ConNF.Litter} {hL : (φ.litterMap L).Dom} {a : ConNF.Atom} (self : φ.MappedOutside L hL a) : a ∈ (φ.litterMap L).get hL

theorem ConNF.BaseLAction.MappedOutside.not_mem_map [ConNF.Params] {φ : ConNF.BaseLAction} {L : ConNF.Litter} {hL : (φ.litterMap L).Dom} {a : ConNF.Atom} (self : φ.MappedOutside L hL a) : a ∉ ConNF.litterSet ((φ.litterMap L).get hL).fst

theorem ConNF.BaseLAction.MappedOutside.not_mem_ran [ConNF.Params] {φ : ConNF.BaseLAction} {L : ConNF.Litter} {hL : (φ.litterMap L).Dom} {a : ConNF.Atom} (self : φ.MappedOutside L hL a) : a ∉ φ.atomMap.ran

theorem ConNF.BaseLAction.mappedOutside_small [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) : ConNF.Small {a : ConNF.Atom | φ.MappedOutside L hL a}

There are only < κ-many atoms in a litter L that are mapped outside the image litter, and that are not already in the domain.

theorem ConNF.BaseLAction.WithoutPreimage.not_mappedOutside [ConNF.Params] (φ : ConNF.BaseLAction) {a : ConNF.Atom} (ha : φ.WithoutPreimage a) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) : ¬φ.MappedOutside L hL a

theorem ConNF.BaseLAction.MappedOutside.not_withoutPreimage [ConNF.Params] (φ : ConNF.BaseLAction) {a : ConNF.Atom} {L : ConNF.Litter} {hL : (φ.litterMap L).Dom} (ha : φ.MappedOutside L hL a) : ¬φ.WithoutPreimage a

theorem ConNF.BaseLAction.mk_mapped_outside_domain [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) : Cardinal.mk ↑(ConNF.litterSet L \ φ.atomMap.Dom) = Cardinal.mk ConNF.κ

The amount of atoms in a litter that are not in the domain already is κ.

def ConNF.BaseLAction.mappedOutsideSubset [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) : Set ConNF.Atom

To each litter we associate a subset which is to contain the atoms mapped outside it.

Equations

• φ.mappedOutsideSubset L hL = ⋯.choose

theorem ConNF.BaseLAction.mappedOutsideSubset_spec [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) : φ.mappedOutsideSubset L hL ⊆ ConNF.litterSet L \ φ.atomMap.Dom ∧ Cardinal.mk ↑(φ.mappedOutsideSubset L hL) = Cardinal.mk ↑{a : ConNF.Atom | φ.MappedOutside L hL a}

theorem ConNF.BaseLAction.mappedOutsideSubset_subset [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) : φ.mappedOutsideSubset L hL ⊆ ConNF.litterSet L

theorem ConNF.BaseLAction.mappedOutsideSubset_closure [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) : φ.mappedOutsideSubset L hL ⊆ φ.atomMap.Domᶜ

theorem ConNF.BaseLAction.mappedOutsideSubset_small [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) : ConNF.Small (φ.mappedOutsideSubset L hL)

theorem ConNF.BaseLAction.mappedOutsideEquiv_def [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) : φ.mappedOutsideEquiv L hL = ⋯.some

@[irreducible]

noncomputable def ConNF.BaseLAction.mappedOutsideEquiv [ConNF.Params] (φ : ConNF.BaseLAction) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) : ↑(φ.mappedOutsideSubset L hL) ≃ ↑{a : ConNF.Atom | φ.MappedOutside L hL a}

A correspondence between the "mapped outside" subset of L and its atoms which were mapped outside the target litter. We will use this equivalence to construct an approximation to use in the freedom of action theorem.

Equations

• @ConNF.BaseLAction.mappedOutsideEquiv = ConNF.BaseLAction.wrapped✝.1

noncomputable def ConNF.BaseLAction.supportedActionAtomMapCore [ConNF.Params] (φ : ConNF.BaseLAction) : ConNF.Atom →. ConNF.Atom

Equations

• One or more equations did not get rendered due to their size.

theorem ConNF.BaseLAction.mem_supportedActionAtomMapCore_dom_iff [ConNF.Params] (φ : ConNF.BaseLAction) (a : ConNF.Atom) : (φ.supportedActionAtomMapCore a).Dom ↔ a ∈ φ.atomMap.Dom ∪ φ.preimageLitterSubset ∪ ⋃ (L : ConNF.Litter), ⋃ (hL : (φ.litterMap L).Dom), φ.mappedOutsideSubset L hL

theorem ConNF.BaseLAction.supportedActionAtomMapCore_dom_eq [ConNF.Params] (φ : ConNF.BaseLAction) : φ.supportedActionAtomMapCore.Dom = φ.atomMap.Dom ∪ φ.preimageLitterSubset ∪ ⋃ (L : ConNF.Litter), ⋃ (hL : (φ.litterMap L).Dom), φ.mappedOutsideSubset L hL

theorem ConNF.BaseLAction.supportedActionAtomMapCore_dom_small [ConNF.Params] (φ : ConNF.BaseLAction) : ConNF.Small φ.supportedActionAtomMapCore.Dom

theorem ConNF.BaseLAction.mk_supportedActionAtomMap_dom [ConNF.Params] (φ : ConNF.BaseLAction) : Cardinal.mk ↑(symmDiff φ.supportedActionAtomMapCore.Dom ((fun (a : ConNF.Atom) => (φ.supportedActionAtomMapCore a).getOrElse (Classical.arbitrary ConNF.Atom)) '' φ.supportedActionAtomMapCore.Dom)) ≤ Cardinal.mk ↑(ConNF.litterSet φ.preimageLitter)

theorem ConNF.BaseLAction.supportedAction_eq_of_dom [ConNF.Params] (φ : ConNF.BaseLAction) {a : ConNF.Atom} (ha : (φ.atomMap a).Dom) : (φ.supportedActionAtomMapCore a).get ⋯ = (φ.atomMap a).get ha

theorem ConNF.BaseLAction.supportedAction_eq_of_mem_preimageLitterSubset [ConNF.Params] (φ : ConNF.BaseLAction) {a : ConNF.Atom} (ha : a ∈ φ.preimageLitterSubset) : (φ.supportedActionAtomMapCore a).get ⋯ = ↑(φ.preimageLitterEquiv ⟨a, ha⟩)

theorem ConNF.BaseLAction.supportedAction_eq_of_mem_mappedOutsideSubset [ConNF.Params] (φ : ConNF.BaseLAction) {a : ConNF.Atom} {L : ConNF.Litter} {hL : (φ.litterMap L).Dom} (ha : a ∈ φ.mappedOutsideSubset L hL) : (φ.supportedActionAtomMapCore a).get ⋯ = ↑((φ.mappedOutsideEquiv L hL) ⟨a, ha⟩)

theorem ConNF.BaseLAction.supportedActionAtomMapCore_injective [ConNF.Params] (φ : ConNF.BaseLAction) ⦃a : ConNF.Atom⦄ ⦃b : ConNF.Atom⦄ (hφ : φ.Lawful) (ha : (φ.supportedActionAtomMapCore a).Dom) (hb : (φ.supportedActionAtomMapCore b).Dom) (hab : (φ.supportedActionAtomMapCore a).get ha = (φ.supportedActionAtomMapCore b).get hb) : a = b

theorem ConNF.BaseLAction.supportedActionAtomMapCore_mem [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) (a : ConNF.Atom) (ha : (φ.supportedActionAtomMapCore a).Dom) (L : ConNF.Litter) (hL : (φ.litterMap L).Dom) : a.1 = L ↔ (φ.supportedActionAtomMapCore a).get ha ∈ (φ.litterMap L).get hL

noncomputable def ConNF.BaseLAction.fillAtomRange [ConNF.Params] (φ : ConNF.BaseLAction) : ConNF.BaseLAction

Equations

• φ.fillAtomRange = { atomMap := φ.supportedActionAtomMapCore, litterMap := φ.litterMap, atomMap_dom_small := ⋯, litterMap_dom_small := ⋯ }

theorem ConNF.BaseLAction.fillAtomRangeLawful [ConNF.Params] (φ : ConNF.BaseLAction) (hφ : φ.Lawful) : φ.fillAtomRange.Lawful

@[simp]

theorem ConNF.BaseLAction.fillAtomRange_atomMap [ConNF.Params] {φ : ConNF.BaseLAction} : φ.fillAtomRange.atomMap = φ.supportedActionAtomMapCore

@[simp]

theorem ConNF.BaseLAction.fillAtomRange_litterMap [ConNF.Params] {φ : ConNF.BaseLAction} : φ.fillAtomRange.litterMap = φ.litterMap

theorem ConNF.BaseLAction.subset_supportedActionAtomMapCore_dom [ConNF.Params] {φ : ConNF.BaseLAction} : φ.atomMap.Dom ⊆ φ.supportedActionAtomMapCore.Dom

theorem ConNF.BaseLAction.subset_supportedActionAtomMapCore_ran [ConNF.Params] {φ : ConNF.BaseLAction} : φ.atomMap.ran ⊆ φ.supportedActionAtomMapCore.ran

theorem ConNF.BaseLAction.fillAtomRange_symmDiff_subset_ran [ConNF.Params] {φ : ConNF.BaseLAction} (hφ : φ.Lawful) (L : ConNF.Litter) (hL : (φ.fillAtomRange.litterMap L).Dom) : symmDiff (↑((φ.fillAtomRange.litterMap L).get hL)) (ConNF.litterSet ((φ.fillAtomRange.litterMap L).get hL).fst) ⊆ φ.fillAtomRange.atomMap.ran