More work on base approximations

Signed-off-by: zeramorphic <[email protected]>

ConNF/Aux/Rel.lean

@@ -76,7 +76,7 @@ theorem codomEqDom_iff' (r : Rel α α) :
     · intro ⟨y, hxy⟩
       exact h₂ x y hxy
 
-theorem OneOne.inv {r : Rel α α} (h : r.OneOne) : r.inv.OneOne :=
+theorem OneOne.inv {r : Rel α β} (h : r.OneOne) : r.inv.OneOne :=
   ⟨⟨h.coinjective⟩, ⟨h.injective⟩⟩
 
 @[simp]
@@ -99,6 +99,59 @@ theorem inv_codom {r : Rel α β} :
     r.inv.codom = r.dom :=
   rfl
 
+@[simp]
+theorem inv_image {r : Rel α β} {s : Set β} :
+    r.inv.image s = r.preimage s :=
+  rfl
+
+@[simp]
+theorem inv_preimage {r : Rel α β} {s : Set α} :
+    r.inv.preimage s = r.image s :=
+  rfl
+
+theorem Injective.image_injective {r : Rel α β} (h : r.Injective) {s t : Set α}
+    (hs : s ⊆ r.dom) (ht : t ⊆ r.dom) (hst : r.image s = r.image t) : s = t := by
+  rw [Set.ext_iff] at hst ⊢
+  intro x
+  constructor
+  · intro hx
+    obtain ⟨y, hxy⟩ := hs hx
+    obtain ⟨z, hz, hzy⟩ := (hst y).mp ⟨x, hx, hxy⟩
+    cases h.injective hxy hzy
+    exact hz
+  · intro hx
+    obtain ⟨y, hxy⟩ := ht hx
+    obtain ⟨z, hz, hzy⟩ := (hst y).mpr ⟨x, hx, hxy⟩
+    cases h.injective hxy hzy
+    exact hz
+
+theorem subset_image_of_preimage_subset {r : Rel α β} {s : Set β} (hs : s ⊆ r.codom) (t : Set α) :
+    r.preimage s ⊆ t → s ⊆ r.image t := by
+  intro hst y hy
+  obtain ⟨x, hx⟩ := hs hy
+  exact ⟨x, hst ⟨y, hy, hx⟩, hx⟩
+
+theorem Injective.preimage_subset_of_subset_image {r : Rel α β} (h : r.Injective)
+    (s : Set β) (t : Set α) :
+    s ⊆ r.image t → r.preimage s ⊆ t := by
+  rintro hst x ⟨y, hy, hxy⟩
+  obtain ⟨z, hz, hzy⟩ := hst hy
+  cases h.injective hzy hxy
+  exact hz
+
+theorem Injective.preimage_subset_iff_subset_image {r : Rel α β} (h : r.Injective)
+    (s : Set β) (hs : s ⊆ r.codom) (t : Set α) :
+    r.preimage s ⊆ t ↔ s ⊆ r.image t :=
+  ⟨subset_image_of_preimage_subset hs t, preimage_subset_of_subset_image h s t⟩
+
+theorem OneOne.preimage_eq_iff_image_eq {r : Rel α β} (h : r.OneOne)
+    {s : Set β} (hs : s ⊆ r.codom) {t : Set α} (ht : t ⊆ r.dom) :
+    r.preimage s = t ↔ r.image t = s := by
+  have h₁ := h.preimage_subset_iff_subset_image s hs t
+  have h₂ := h.inv.preimage_subset_iff_subset_image t ht s
+  rw [preimage_inv, inv_image] at h₂
+  rw [subset_antisymm_iff, subset_antisymm_iff, h₁, h₂, and_comm]
+
 theorem CodomEqDom.inv {r : Rel α α} (h : r.CodomEqDom) : r.inv.CodomEqDom := by
   rw [codomEqDom_iff] at h ⊢
   exact h.symm
@@ -139,6 +192,15 @@ theorem preimage_codom {r : Rel α β} :
     r.preimage r.codom = r.dom :=
   image_dom
 
+theorem preimage_subset_dom (r : Rel α β) (t : Set β) :
+    r.preimage t ⊆ r.dom := by
+  rintro x ⟨y, _, h⟩
+  exact ⟨y, h⟩
+
+theorem image_subset_codom (r : Rel α β) (s : Set α) :
+    r.image s ⊆ r.codom :=
+  r.inv.preimage_subset_dom s
+
 theorem image_empty_of_disjoint_dom {r : Rel α β} {s : Set α} (h : Disjoint r.dom s) :
     r.image s = ∅ := by
   rw [eq_empty_iff_forall_not_mem]

ConNF/FOA/BaseApprox.lean

@@ -228,7 +228,6 @@ theorem typical_image_sublitter (ψ : BaseApprox) {L₁ L₂ : Litter} (h : ψ
     · convert typical.mk L₁ L₂ h ((nearLitterEquiv (ψ.sublitter L₂)).symm ⟨a, ha⟩) using 1
       rw [Equiv.apply_symm_apply]
 
--- TODO: In the blueprint we required `s ⊆ ψᴬ.dom`.
 theorem image_near_of_near (ψ : BaseApprox) (s : Set Atom)
     {L₁ L₂ : Litter} (hL : ψᴸ L₁ L₂) (hsL : s ~ L₁ᴬ) :
     ψᴬ.image s ~ L₂ᴬ := by
@@ -249,7 +248,61 @@ theorem image_near_of_near (ψ : BaseApprox) (s : Set Atom)
     _ ~ L₂ᴬ := (ψ.sublitter L₂).atoms_near_litter
 
 def nearLitters (ψ : BaseApprox) : Rel NearLitter NearLitter :=
-  λ N₁ N₂ ↦ ψᴸ N₁ᴸ N₂ᴸ ∧ ψᴬ.image N₁ᴬ = N₂ᴬ
+  λ N₁ N₂ ↦ ψᴸ N₁ᴸ N₂ᴸ ∧ N₁ᴬ ⊆ ψᴬ.dom ∧ ψᴬ.image N₁ᴬ = N₂ᴬ
+
+instance : SuperN BaseApprox (Rel NearLitter NearLitter) where
+  superN := nearLitters
+
+theorem nearLitters_def (ψ : BaseApprox) {N₁ N₂ : NearLitter} :
+    ψᴺ N₁ N₂ ↔ ψᴸ N₁ᴸ N₂ᴸ ∧ N₁ᴬ ⊆ ψᴬ.dom ∧ ψᴬ.image N₁ᴬ = N₂ᴬ :=
+  Iff.rfl
+
+@[simp]
+theorem inv_nearLitters (ψ : BaseApprox) : ψ⁻¹ᴺ = ψᴺ.inv := by
+  ext N₁ N₂
+  rw [inv_def, nearLitters_def, nearLitters_def, inv_litters, inv_def, inv_atoms,
+    and_congr_right_iff, inv_image]
+  intro
+  constructor
+  · rintro ⟨h₁, h₂⟩
+    have := h₂.symm.trans_subset (ψᴬ.preimage_subset_dom N₁ᴬ)
+    exact ⟨this, (ψ.atoms_permutative.preimage_eq_iff_image_eq h₁ this).mp h₂⟩
+  · rintro ⟨h₁, h₂⟩
+    have := h₂.symm.trans_subset (ψᴬ.image_subset_codom N₂ᴬ)
+    exact ⟨this, (ψ.atoms_permutative.preimage_eq_iff_image_eq this h₁).mpr h₂⟩
+
+theorem atoms_subset_dom_of_nearLitters_left {ψ : BaseApprox} {N₁ N₂ : NearLitter} (h : ψᴺ N₁ N₂) :
+    N₁ᴬ ⊆ ψᴬ.dom :=
+  h.2.1
+
+theorem atoms_subset_dom_of_nearLitters_right {ψ : BaseApprox} {N₁ N₂ : NearLitter} (h : ψᴺ N₁ N₂) :
+    N₂ᴬ ⊆ ψᴬ.dom := by
+  have := atoms_subset_dom_of_nearLitters_left (show ψ⁻¹ᴺ N₂ N₁ from ψ.inv_nearLitters ▸ h)
+  rwa [inv_atoms, inv_dom, ψ.atoms_permutative.codom_eq_dom] at this
+
+theorem nearLitters_injective (ψ : BaseApprox) : ψᴺ.Injective := by
+  constructor
+  intro N₁ N₂ N₃ h₁ h₂
+  rw [nearLitters_def] at h₁ h₂
+  apply NearLitter.ext
+  apply ψ.atoms_permutative.image_injective h₁.2.1 h₂.2.1
+  exact h₁.2.2.trans h₂.2.2.symm
+
+theorem nearLitters_coinjective (ψ : BaseApprox) : ψᴺ.Coinjective := by
+  have := ψ⁻¹.nearLitters_injective
+  rwa [inv_nearLitters, inv_injective_iff] at this
+
+theorem nearLitters_codom_subset_dom (ψ : BaseApprox) : ψᴺ.codom ⊆ ψᴺ.dom := by
+  rintro N₂ ⟨N₁, h⟩
+  obtain ⟨L₃, hL₃⟩ := ψ.litters_permutative.mem_dom h.1
+  use ⟨L₃, ψᴬ.image N₂ᴬ, ψ.image_near_of_near N₂ᴬ hL₃ N₂.atoms_near_litter⟩
+  exact ⟨hL₃, atoms_subset_dom_of_nearLitters_right h, rfl⟩
+
+theorem nearLitters_permutative (ψ : BaseApprox) : ψᴺ.Permutative := by
+  refine ⟨⟨ψ.nearLitters_injective, ψ.nearLitters_coinjective⟩,
+    ⟨subset_antisymm ψ.nearLitters_codom_subset_dom ?_⟩⟩
+  have := ψ⁻¹.nearLitters_codom_subset_dom
+  rwa [inv_nearLitters] at this
 
 end BaseApprox
 

blueprint/src/chapters/foa.tex

@@ -2,6 +2,8 @@ \section{Base approximations}
 \begin{definition}[base approximation]
   \label{def:BaseApprox}
   \uses{def:NearLitter}
+  \lean{ConNF.BaseApprox}
+  \leanok
   A \emph{base approximation} is a pair \( \psi = (\psi^{E\Atom}, \psi^\Litter) \) such that \( \psi^{E\Atom} \) and \( \psi^\Litter \) are permutative relations of atoms and litters respectively (\cref{def:relation_props}), and for each litter \( L \), the set
   \[ \LS(L) \cap \coim \psi^{E\Atom} \]
   is small.
@@ -16,6 +18,8 @@ \section{Base approximations}
 \begin{definition}[atom graph of an approximation]
   \uses{def:BaseApprox}
   \label{def:atomGraph}
+  \lean{ConNF.BaseApprox.atoms}
+  \leanok
   The \emph{typical atom graph} of \( \psi \) is the relation \( \psi^{T\Atom} \) given by the following constructor.
   If \( (L_1, L_2) \in \psi^\Litter \), then
   \[ (h_{(L_1)_\psi}(i), h_{(L_2)_\psi}(i)) \in \psi^{T\Atom} \]
@@ -26,18 +30,24 @@ \section{Base approximations}
 \begin{proposition}
   \uses{def:atomGraph}
   \label{prop:atomGraph_inv}
+  \lean{ConNF.BaseApprox.instInv}
+  \leanok
   \( (\psi^{T\Atom})^{-1} = (\psi^{-1})^{T\Atom} \) and hence \( (\psi^\Atom)^{-1} = (\psi^{-1})^\Atom \).
 \end{proposition}
 \begin{proof}
+  \leanok
   This follows directly from the fact that \( L_\psi = L_{\psi^{-1}} \) for any litter \( L \).
 \end{proof}
 \begin{proposition}
   \uses{def:atomGraph}
   \label{prop:atomGraph_permutative}
+  \lean{ConNF.BaseApprox.typical_permutative,ConNF.BaseApprox.atoms_permutative}
+  \leanok
   The graphs \( \psi^{T\Atom} \) and \( \psi^\Atom \) are permutative.
 \end{proposition}
 \begin{proof}
   \uses{prop:atomGraph_inv}
+  \leanok
   The typical atom graph is injective, because the equation \( h_{L_\psi}(i)^\circ = L \) can be used to establish the the parameters of the relevant \( h \) maps coincide.
   Furthermore, we can use the fact that \( \psi^\Litter \) has equal image and coimage to produce images of any image element of this relation.
   We then appeal to symmetry using \cref{prop:atomGraph_inv} to conclude that \( \psi^{T\Atom} \) is permutative.
@@ -69,15 +79,20 @@ \section{Base approximations}
 \begin{definition}[near-litter graph of an approximation]
   \uses{def:atomGraph}
   \label{def:nearLitterGraph}
+  \lean{ConNF.BaseApprox.nearLitters}
+  \leanok
   The \emph{near-litter graph} of \( \psi \) is the relation \( \psi^\NearLitter \) given by setting \( (N_1, N_2) \in \psi^\NearLitter \) if and only if \( (N_1^\circ, N_2^\circ) \in \psi^\Litter \), \( N_1 \) and \( N_2 \) are subsets of \( \coim \psi^\Atom \), and the image of \( \psi^\Atom \) on \( N_1 \) is \( N_2 \) (or equivalently, by \cref{prop:relation_results}, the coimage of \( \psi^\Atom \) on \( N_2 \) is \( N_1 \)).
 \end{definition}
 \begin{proposition}
   \uses{def:nearLitterGraph}
   \label{prop:approx_near}
+  \lean{ConNF.BaseApprox.image_near_of_near}
+  \leanok
   Let \( s \) be a set of atoms near \( \LS(L) \) for some litter \( L \).
-  If \( s \subseteq \coim \psi^\Atom \) and \( (L, L') \in \psi^\Litter \), then the image of \( \psi^\Atom \) on \( s \) is near \( \LS(L') \).
+  If \( (L, L') \in \psi^\Litter \), then the image of \( \psi^\Atom \) on \( s \) is near \( \LS(L') \).
 \end{proposition}
 \begin{proof}
+  \leanok
   We calculate
   \begin{align*}
     \im \psi^\Atom|_s
@@ -89,15 +104,17 @@ \section{Base approximations}
     &= L'_\psi \\
     &\near \LS(L')
   \end{align*}
-  Many of these equalities should be their own lemmas.
 \end{proof}
 \begin{proposition}
   \uses{def:nearLitterGraph}
   \label{prop:nearLitterGraph_permutative}
+  \lean{ConNF.BaseApprox.inv_nearLitters,ConNF.BaseApprox.nearLitters_permutative}
+  \leanok
   \( (\psi^{-1})^\NearLitter = (\psi^\NearLitter)^{-1} \), and \( \psi^\NearLitter \) is permutative.
 \end{proposition}
 \begin{proof}
   \uses{prop:atomGraph_permutative,prop:approx_near}
+  \leanok
   The first part follows from \cref{prop:atomGraph_inv}.
   To show \( \psi^\NearLitter \) is permutative, it suffices to show that it is injective and that its image is contained in its coimage; then, by taking inverses, the converses will also hold.
   Suppose that \( (N_1, N_3), (N_2, N_3) \in \psi^\NearLitter \).
@@ -353,6 +370,8 @@ \section{Base actions}
 \begin{definition}
   \uses{def:NearLitter}
   \label{def:Interference}
+  \lean{ConNF.Interference}
+  \leanok
   The \emph{interference} of near-litters \( N_1, N_2 \) is
   \[ \interf(N_1, N_2) = \begin{cases}
     N_1 \symmdiff N_2 & \text{if } N_1^\circ = N_2^\circ \\