source.lean

1 import KomorebiPaperIII.NonlinearPacketCoordinates
2 import KomorebiPaperIII.PacketDirectSum
3 import Mathlib.Tactic.FinCases
4 import Mathlib.Tactic.NormNum
5 
6 /-! External consumers, not production theorem-count additions. -/
7 set_option autoImplicit false
8 noncomputable section
9 open scoped BigOperators
10 open Komorebi.PaperIII.PacketCoordinates
11 namespace PaperIIIBoundary
12 
13 abbrev V := ℚ × ℚ
14 
15 def oblique0 : V →ₗ[ℚ] V where
16   toFun x := (x.1 + x.2, 0)
17   map_add' x y := by apply Prod.ext <;> simp [add_left_comm, add_comm]
18   map_smul' c x := by apply Prod.ext <;> simp [mul_add]
19 
20 def oblique1 : V →ₗ[ℚ] V where
21   toFun x := (-x.2, x.2)
22   map_add' x y := by apply Prod.ext <;> simp [add_comm]
23   map_smul' c x := by apply Prod.ext <;> simp
24 
25 def oblique : System ℚ V (Fin 2) where
26   projector i := if i = 0 then oblique0 else oblique1
27   complete := by
28     apply LinearMap.ext
29     intro x
30     apply Prod.ext <;> simp [Fin.sum_univ_two, oblique0, oblique1]
31   idempotent i := by
32     fin_cases i <;> apply LinearMap.ext <;> intro x <;> apply Prod.ext <;>
33       simp [oblique0, oblique1]
34   orthogonal i j h := by
35     fin_cases i <;> fin_cases j <;> try contradiction
36     all_goals apply LinearMap.ext
37     all_goals intro x
38     all_goals apply Prod.ext <;> simp [oblique0, oblique1]
39 
40 example : (oblique.analysis (2, 3) 0 : V) = (5, 0) := by
41   norm_num [oblique, System.analysis, oblique0]
42 example : (oblique.analysis (2, 3) 1 : V) = (-3, 3) := by
43   norm_num [oblique, System.analysis, oblique1]
44 
45 example (x : V) : oblique.synthesis (oblique.analysis x) = x := oblique.synthesis_analysis x
46 example (z : oblique.Coordinates) : oblique.analysis (oblique.synthesis z) = z :=
47   oblique.analysis_synthesis z
48 example (x : V) (i : Fin 2) : (oblique.directSumEquiv x i : V) = oblique.projector i x :=
49   oblique.directSumEquiv_component x i
50 
51 def mixed (x : V) : V := (x.1 * x.2, x.1^2 + x.2)
52 example : mixed (2, 3) = (6, 7) := by norm_num [mixed]
53 example : mixed (2, 3) ≠ ((mixed (2, 0)).1, (mixed (0, 3)).2) := by norm_num [mixed]
54 example : oblique.synthesis (coordinateMap oblique oblique mixed (oblique.analysis (2, 3))) = (6, 7) := by
55   rw [coordinateMap_analysis, oblique.synthesis_analysis]
56   norm_num [mixed]
57 example (f g : V → V) : coordinateMap oblique oblique (g ∘ f) =
58     coordinateMap oblique oblique g ∘ coordinateMap oblique oblique f :=
59   coordinateMap_comp oblique oblique oblique f g
60 example (f : V → V) (n : Nat) (x : V) :
61     (coordinateMap oblique oblique f)^[n] (oblique.analysis x) = oblique.analysis x ↔
62       (f^[n]) x = x := periodicPoint_iff oblique f n x
63 
64 -- The advertised result requires neither scalar commutativity nor additive inverses.
65 universe u v w
66 example {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M]
67     {I : Type w} [Fintype I] (P : System R M I) (x : M) :
68     P.synthesis (P.analysis x) = x := P.synthesis_analysis x
69 
70 end PaperIIIBoundary

Back to source controls