Section88Reference.lean

1 import KomorebiLSM.PerturbedOperatorFixture
2 import KomorebiLSM.InteriorRepair
3 
4 /-! The actual unmodified fixture is positive on the predecessor comparison cone. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.Section88Reference
7 open scoped BigOperators
8 open LorentzCylinder RationalBernsteinMargin RationalLorentzMatrix PerturbedOperatorFixture
9 open RobustOrientedMargin ContinuousInstrument MeasureTheory
10 noncomputable section
11 
12 def operator (a : Bool) (u : ℝ) : State ℂ →L[ℝ] State ℂ :=
13   PolynomialGram.operatorPolynomial (fun k => matrixOperator (referenceComparison a k)) u
14 
15 theorem coordinate_operator (a : Bool) (u : ℝ) (z : State ℂ) (i : Fin 3) :
16     coordinate i (operator a u z)=∑ k : Fin 3,u^(k : ℕ)*
17       (∑ j : Fin 3,(referenceComparison a k i j : ℝ)*coordinate j z) := by
18   simp only [operator,PolynomialGram.operatorPolynomial,sum_apply,smul_apply,map_sum,map_smul,
19     coordinate_matrixOperator,smul_eq_mul]
20 
21 theorem direct_mass (u : ℝ) (z : State ℂ) :
22     (operator false u z).1=(1/4+9/4*u^2)*z.1+u*(6/5*z.2.re+9/10*z.2.im) := by
23   change coordinate 0 (operator false u z)=_
24   rw [coordinate_operator]
25   norm_num [Fin.sum_univ_succ,coordinate,Matrix.cons_val_two]
26   ring
27 
28 theorem direct_real (u : ℝ) (z : State ℂ) :
29     (operator false u z).2.re=6/5*u*z.1+(1/4+63/100*u^2)*z.2.re+54/25*u^2*z.2.im := by
30   change coordinate 1 (operator false u z)=_
31   rw [coordinate_operator]
32   norm_num [Fin.sum_univ_succ,coordinate,Matrix.cons_val_two]
33   ring
34 
35 theorem direct_imag (u : ℝ) (z : State ℂ) :
36     (operator false u z).2.im=9/10*u*z.1+54/25*u^2*z.2.re+(1/4-63/100*u^2)*z.2.im := by
37   change coordinate 2 (operator false u z)=_
38   rw [coordinate_operator]
39   norm_num [Fin.sum_univ_succ,coordinate,Matrix.cons_val_two]
40   ring
41 
42 /-- Exact conformal quadratic identity for the full observation polynomial. -/
43 theorem direct_quadratic (u : ℝ) (z : State ℂ) :
44     (operator false u z).1^2-(operator false u z).2.re^2-(operator false u z).2.im^2=
45       ((1-9*u^2)/4)^2*(z.1^2-z.2.re^2-z.2.im^2) := by
46   rw [direct_mass,direct_real,direct_imag]
47   ring
48 
49 theorem direct_normalized_positive (u : ℝ) (v : ℂ) (hv : ‖v‖≤1) : operator false u (1,v)∈cone := by
50   have hsq : v.re^2+v.im^2≤1 := by
51     have he := Complex.normSq_eq_norm_sq v
52     simp only [Complex.normSq_apply,pow_two] at he
53     nlinarith [norm_nonneg v]
54   let d : ℝ := 4/5*v.re+3/5*v.im
55   have hd : |d|≤1 := by
56     apply (sq_le_sq₀ (abs_nonneg _) (by norm_num : (0 : ℝ)≤1)).mp
57     rw [sq_abs]
58     dsimp [d]
59     nlinarith [sq_nonneg (3/5*v.re-4/5*v.im)]
60   let b : ℝ := 3*u/2
61   have hm : (operator false u (1,v)).1=1/4+b^2+b*d := by
62     rw [direct_mass]
63     dsimp [b,d]
64     ring
65   have hb : |b*d|≤|b| := by
66     rw [abs_mul]
67     simpa using mul_le_mul_of_nonneg_left hd (abs_nonneg b)
68   have hm0 : 0≤(operator false u (1,v)).1 := by
69     rw [hm]
70     nlinarith [neg_abs_le (b*d),sq_abs b,sq_nonneg (|b|-1/2)]
71   have hquad : 0≤(operator false u (1,v)).1^2-(operator false u (1,v)).2.re^2-
72       (operator false u (1,v)).2.im^2 := by
73     rw [direct_quadratic]
74     exact mul_nonneg (sq_nonneg _) (by norm_num; linarith)
75   change ‖(operator false u (1,v)).2‖≤(operator false u (1,v)).1
76   apply (sq_le_sq₀ (norm_nonneg _) hm0).mp
77   rw [← Complex.normSq_eq_norm_sq,Complex.normSq_apply]
78   nlinarith
79 
80 def rotation : RationalMatrix := ![![1,0,0],![0,3/5,4/5],![0,-4/5,3/5]]
81 
82 theorem rotation_action (z : State ℂ) :
83     matrixOperator rotation z=(z.1,(⟨3/5,-4/5⟩ : ℂ)*z.2) := by
84   apply coordinate_ext
85   intro i
86   simp only [coordinate_matrixOperator]
87   fin_cases i <;> norm_num [rotation,coordinate,Fin.sum_univ_succ,Matrix.cons_val_two]
88   ring
89 
90 theorem rotation_positive {z : State ℂ} (hz : z∈cone) : matrixOperator rotation z∈cone := by
91   rw [rotation_action]
92   change ‖(⟨3/5,-4/5⟩ : ℂ)*z.2‖≤z.1
93   rw [norm_mul]
94   have hn : ‖(⟨3/5,-4/5⟩ : ℂ)‖=1 := by
95     have h := Complex.normSq_eq_norm_sq (⟨3/5,-4/5⟩ : ℂ)
96     norm_num [Complex.normSq_apply] at h
97     nlinarith [norm_nonneg (⟨3/5,-4/5⟩ : ℂ)]
98   simpa [hn] using hz
99 
100 theorem rotated_action (u : ℝ) (z : State ℂ) :
101     operator true u z=operator false u (matrixOperator rotation z) := by
102   apply coordinate_ext
103   intro i
104   simp only [coordinate_operator,coordinate_matrixOperator]
105   fin_cases i <;> norm_num [rotation,coordinate,Fin.sum_univ_succ,Matrix.cons_val_two] <;> first | trivial | (ring <;> simp)
106 
107 theorem positive (a : Bool) (u : ℝ) {z : State ℂ} (hz : z∈cone) : operator a u z∈cone := by
108   have hd : ∀ w∈cone,operator false u w∈cone :=
109     fun w hw => preserves_of_normalized (operator false u) (direct_normalized_positive u) hw
110   cases a
111   · exact hd z hz
112   · rw [rotated_action]
113     exact hd _ (rotation_positive hz)
114 
115 theorem moment_mass (a : Bool) (z : State ℂ) :
116     probabilityCone.mass ((∑ k : Fin 3,UniformIntervalMoments.moment k •
117       matrixOperator (referenceComparison a k)) z)=probabilityCone.mass z := by
118   change coordinate 0 ((∑ k : Fin 3,UniformIntervalMoments.moment k •
119     matrixOperator (referenceComparison a k)) z)=z.1
120   simp only [sum_apply,smul_apply,map_sum,map_smul,coordinate_matrixOperator]
121   cases a <;> norm_num [Fin.sum_univ_succ,coordinate,UniformIntervalMoments.moment_formula,Matrix.cons_val_two] <;> ring
122 
123 def instrument : DensityInstrument (A := Bool) (probabilityCone (V := ℂ)) UniformIntervalMoments.measure where
124   op := operator
125   measurable_op a := (PolynomialGram.operatorPolynomial_continuous _).measurable
126   integrable_op a := PolynomialGram.operatorPolynomial_integrable _
127   positive a := by
128     filter_upwards [] with u
129     exact fun z hz => positive a u hz
130   mass_preserving a z := by
131     change probabilityCone.mass ((∫ u,PolynomialGram.operatorPolynomial
132       (fun k => matrixOperator (referenceComparison a k)) u∂UniformIntervalMoments.measure) z)=_
133     rw [PolynomialGram.operatorPolynomial_integral]
134     exact moment_mass a z
135 
136 end
137 end Komorebi.LSM.Section88Reference

Back to source controls