SharedCorrectionControls.lean

1 module
2 
3 public import SharedCorrection
4 public import Mathlib.Data.ZMod.Basic
5 public import Mathlib.Tactic.NormNum
6 
7 @[expose] public section
8 noncomputable section
9 set_option autoImplicit false
10 
11 namespace Komorebi.SharedCorrectionControls
12 
13 open SharedCorrection
14 
15 abbrev Two := ZMod 2
16 abbrev identity : Two →ₗ[Two] Two := LinearMap.id
17 abbrev leftCoordinate : (Two × Two) →ₗ[Two] Two := LinearMap.fst Two Two Two
18 abbrev rightCoordinate : (Two × Two) →ₗ[Two] Two := LinearMap.snd Two Two Two
19 
20 /-- Separate solvability does not imply that one correction solves both targets. -/
21 theorem separately_solvable_but_incompatible :
22     (∃ u : Two, identity u = 0) ∧ (∃ v : Two, identity v = 1) ∧
23       ¬ ∃ w : Two, identity w = 0 ∧ identity w = 1 := by
24   refine ⟨⟨0, rfl⟩, ⟨1, rfl⟩, ?_⟩
25   rintro ⟨w, hw0, hw1⟩
26   have h : (0 : Two) = 1 := hw0.symm.trans hw1
27   norm_num at h
28 
29 /-- The common quotient detects that incompatibility for the actual two maps. -/
30 theorem identical_maps_distinguish_targets :
31     (Submodule.Quotient.mk (0 : Two) : Common identity identity) ≠
32       Submodule.Quotient.mk (1 : Two) := by
33   intro h
34   have hw := (quotient_mk_eq_iff_common identity identity 0 1).mp h
35   exact separately_solvable_but_incompatible.2.2 hw
36 
37 /-- Independent coordinates admit a common correction for every pair of targets. -/
38 theorem independent_targets_have_equal_labels (a b : Two) :
39     (Submodule.Quotient.mk (a, 0) : Common leftCoordinate rightCoordinate) =
40       Submodule.Quotient.mk (0, b) := by
41   apply (quotient_mk_eq_iff_common leftCoordinate rightCoordinate (a, 0) (0, b)).mpr
42   exact ⟨(a, b), rfl, rfl⟩
43 
44 /-- For independent coordinates the joint image fills the entire product of ranges. -/
45 theorem independent_joint_range_top :
46     LinearMap.range (joint leftCoordinate rightCoordinate) = ⊤ := by
47   ext z
48   simp only [Submodule.mem_top, iff_true]
49   refine ⟨(z.1.val, z.2.val), ?_⟩
50   apply Prod.ext <;> apply Subtype.ext <;> rfl
51 
52 /-- A zero left map contributes no compatibility restriction. -/
53 theorem zero_left_identifies_all (u v : Two) :
54     (Submodule.Quotient.mk u : Common (0 : Two →ₗ[Two] Two) identity) =
55       Submodule.Quotient.mk v := by
56   apply (quotient_mk_eq_iff_common (0 : Two →ₗ[Two] Two) identity u v).mpr
57   exact ⟨v, rfl, rfl⟩
58 
59 /-- Evaluation of an arbitrary sequence at a specified coordinate. -/
60 def evaluateCoordinate (n : ℕ) : (ℕ → Two) →ₗ[Two] Two where
61   toFun f := f n
62   map_add' _ _ := rfl
63   map_smul' _ _ := rfl
64 
65 /-- Finite local target implies a finite quotient even for the full sequence domain. -/
66 theorem sequence_domain_common_finite :
67     Infinite (ℕ → Two) ∧ Finite (Common (evaluateCoordinate 0) (evaluateCoordinate 1)) := by
68   constructor
69   · infer_instance
70   · exact common_finite_of_left (evaluateCoordinate 0) (evaluateCoordinate 1)
71 
72 end Komorebi.SharedCorrectionControls
73 
74 #print axioms Komorebi.SharedCorrectionControls.separately_solvable_but_incompatible
75 #print axioms Komorebi.SharedCorrectionControls.identical_maps_distinguish_targets
76 #print axioms Komorebi.SharedCorrectionControls.independent_targets_have_equal_labels
77 #print axioms Komorebi.SharedCorrectionControls.independent_joint_range_top
78 #print axioms Komorebi.SharedCorrectionControls.zero_left_identifies_all
79 #print axioms Komorebi.SharedCorrectionControls.sequence_domain_common_finite

Back to source controls