AffinePairControls.lean

1 module
2 public import AffineSharedCorrection
3 public import Mathlib.Tactic.NormNum
4 
5 @[expose] public section
6 set_option autoImplicit false
7 
8 namespace Komorebi.AffinePairControls
9 open Komorebi.NativeAffine Komorebi.AffinePair
10 
11 abbrev oneId : (Fin 1 → ℤ) →ₗ[ℤ] (Fin 1 → ℤ) := LinearMap.id
12 
13 /-- Two individually solvable congruences need not have a common lift. -/
14 theorem two_individual_lifts :
15     (∃ y : ℤ, (4 : ℤ) ∣ y) ∧ (∃ y : ℤ, (4 : ℤ) ∣ y - 2) := by
16   exact ⟨⟨0, dvd_zero _⟩, ⟨2, by norm_num⟩⟩
17 
18 theorem incompatible_mod_four :
19     ¬ HasJointLift 2 1 oneId oneId (fun _ => 0) (fun _ => 2) (fun _ => 0) := by
20   rintro ⟨y, _, hA, hB⟩
21   have h0 := hA 0
22   have h2 := hB 0
23   norm_num [oneId] at h0 h2
24   omega
25 
26 /-- The theorem's allowed composite-modulus and level-zero endpoint is real. -/
27 theorem composite_level_zero :
28     HasJointLift 4 0 oneId oneId (fun _ => 5) (fun _ => 9) (fun _ => 0) := by
29   refine ⟨fun _ => 1, ?_, ?_, ?_⟩ <;> intro i <;> norm_num [oneId]
30 
31 theorem modulus_one (d e f L : ℕ)
32     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
33     (B : (Fin d → ℤ) →ₗ[ℤ] (Fin f → ℤ))
34     (b : Fin e → ℤ) (c : Fin f → ℤ) (x : Fin d → ℤ) :
35     HasJointLift 1 L A B b c x := by
36   refine ⟨x, ?_, ?_, ?_⟩ <;> intro i <;> simp
37 
38 end Komorebi.AffinePairControls
39 
40 #print axioms Komorebi.AffinePairControls.oneId
41 #print axioms Komorebi.AffinePairControls.two_individual_lifts
42 #print axioms Komorebi.AffinePairControls.incompatible_mod_four
43 #print axioms Komorebi.AffinePairControls.composite_level_zero
44 #print axioms Komorebi.AffinePairControls.modulus_one

Back to source controls