Lifting.lean

1 import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
2 import Mathlib.LinearAlgebra.Matrix.Notation
3 import Mathlib.Tactic
4 
5 /-!
6 Author: Komorebi P.
7 Checked source. Exact pair and coordinatewise lifting.
8 The normalized Haar transform and its l2 energy theorem are separate obligations.
9 -/
10 
11 namespace KomorebiPaperV
12 section Lifting
13 variable {K : Type*} [Field K] [CharZero K]
14 
15 def liftingAnalysis (x : K × K) : K × K :=
16   (x.1 + (x.2 - x.1) / 2, x.2 - x.1)
17 
18 def liftingSynthesis (y : K × K) : K × K :=
19   (y.1 - y.2 / 2, y.2 + (y.1 - y.2 / 2))
20 
21 theorem lifting_synthesis_analysis (x : K × K) :
22     liftingSynthesis (liftingAnalysis x) = x := by
23   apply Prod.ext <;> dsimp [liftingAnalysis, liftingSynthesis] <;> ring
24 
25 theorem lifting_analysis_synthesis (y : K × K) :
26     liftingAnalysis (liftingSynthesis y) = y := by
27   apply Prod.ext <;> dsimp [liftingAnalysis, liftingSynthesis] <;> ring
28 
29 theorem lifting_determinant :
30     Matrix.det (!![(1 / 2 : K), 1 / 2; -1, 1]) = 1 := by
31   norm_num [Matrix.det_fin_two]
32 
33 def liftingEquiv : (K × K) ≃ (K × K) where
34   toFun := liftingAnalysis
35   invFun := liftingSynthesis
36   left_inv := lifting_synthesis_analysis
37   right_inv := lifting_analysis_synthesis
38 
39 theorem lifting_coordinates_roundtrip {I : Type*} (x : I → K × K) :
40     (fun i => liftingSynthesis (liftingAnalysis (x i))) = x := by
41   funext i
42   exact lifting_synthesis_analysis (x i)
43 end Lifting
44 end KomorebiPaperV

Back to source controls