ComplexCoefficientBox.lean

1 import KomorebiLSM.RationalBernsteinMargin
2 
3 /-! Real entry budgets in the actual mass/real/imaginary coordinates. -/
4 set_option autoImplicit false
5 namespace Komorebi.LSM.ComplexCoefficientBox
6 open LorentzCylinder RobustOrientedMargin
7 open scoped BigOperators
8 abbrev RealMatrix := Matrix (Fin 3) (Fin 3) ℝ
9 
10 noncomputable def row (E : RealMatrix) (i : Fin 3) : State ℂ →L[ℝ] ℝ :=
11   ∑ j,E i j • RationalBernsteinMargin.coordinate j
12 
13 noncomputable def matrixOperator (E : RealMatrix) : State ℂ →L[ℝ] State ℂ :=
14   (row E 0).prod (Complex.equivRealProdCLM.symm.toContinuousLinearMap.comp
15     ((row E 1).prod (row E 2)))
16 
17 @[simp] theorem coordinate_matrixOperator (E : RealMatrix) (i : Fin 3) (z : State ℂ) :
18     RationalBernsteinMargin.coordinate i (matrixOperator E z)=
19       ∑ j,E i j*RationalBernsteinMargin.coordinate j z := by
20   fin_cases i <;> simp [RationalBernsteinMargin.coordinate,matrixOperator,row]
21 
22 @[simp] theorem matrixOperator_rat (E : RationalBernsteinMargin.RationalMatrix) :
23     matrixOperator (fun i j => (E i j : ℝ))=RationalBernsteinMargin.matrixOperator E := rfl
24 
25 theorem normalized_coordinate_bound (v : ℂ) (hv : ‖v‖≤1) (i : Fin 3) :
26     |RationalBernsteinMargin.coordinate i (1,v)|≤1 := by
27   fin_cases i
28   · norm_num [RationalBernsteinMargin.coordinate]
29   · exact (Complex.abs_re_le_norm v).trans hv
30   · exact (Complex.abs_im_le_norm v).trans hv
31 
32 theorem row_bound (E : RealMatrix) (v : ℂ) (hv : ‖v‖≤1) (i : Fin 3) :
33     |RationalBernsteinMargin.coordinate i (matrixOperator E (1,v))|≤∑ j,|E i j| := by
34   rw [coordinate_matrixOperator]
35   calc
36     _ ≤ ∑ j : Fin 3,|E i j*RationalBernsteinMargin.coordinate j (1,v)| := Finset.abs_sum_le_sum_abs _ _
37     _ ≤ _ := by
38       apply Finset.sum_le_sum
39       intro j _
40       rw [abs_mul]
41       exact (mul_le_mul_of_nonneg_left (normalized_coordinate_bound v hv j) (abs_nonneg _)).trans_eq (mul_one _)
42 
43 theorem value_bound (E : RealMatrix) (v : ℂ) (hv : ‖v‖≤1) :
44     probabilityCone.value (matrixOperator E (1,v))≤
45       max (∑ j,|E 0 j|) ((∑ j,|E 1 j|)+(∑ j,|E 2 j|)) := by
46   rw [value_eq]
47   apply max_le_max (row_bound E v hv 0)
48   exact (Complex.norm_le_abs_re_add_abs_im _).trans (add_le_add (row_bound E v hv 1) (row_bound E v hv 2))
49 
50 theorem entry_row_bound (E : RealMatrix) (r : ℝ) (hE : ∀ i j,|E i j|≤r) (i : Fin 3) :
51     (∑ j,|E i j|)≤3*r := by
52   calc
53     _ ≤ ∑ _j : Fin 3,r := Finset.sum_le_sum fun j _ => hE i j
54     _ = _ := by simp
55 
56 theorem coefficient_output_bounds (E : RealMatrix) (r : ℝ) (hE : ∀ i j,|E i j|≤r)
57     (v : ℂ) (hv : ‖v‖≤1) :
58     |(matrixOperator E (1,v)).1|≤3*r ∧ ‖(matrixOperator E (1,v)).2‖≤6*r := by
59   have h0 := (row_bound E v hv 0).trans (entry_row_bound E r hE 0)
60   have h1 := (row_bound E v hv 1).trans (entry_row_bound E r hE 1)
61   have h2 := (row_bound E v hv 2).trans (entry_row_bound E r hE 2)
62   refine ⟨h0,?_⟩
63   have hn := Complex.norm_le_abs_re_add_abs_im (matrixOperator E (1,v)).2
64   change |(matrixOperator E (1,v)).2.re|≤3*r at h1
65   change |(matrixOperator E (1,v)).2.im|≤3*r at h2
66   linarith
67 
68 theorem polynomial_coordinate {n : ℕ} (E : Fin n → RealMatrix) (u : ℝ) (z : State ℂ) (i : Fin 3) :
69     RationalBernsteinMargin.coordinate i (PolynomialGram.operatorPolynomial (fun k => matrixOperator (E k)) u z)=
70       ∑ k : Fin n,u^(k : ℕ)*RationalBernsteinMargin.coordinate i (matrixOperator (E k) z) := by
71   simp only [PolynomialGram.operatorPolynomial,sum_apply,smul_apply,map_sum,map_smul]
72   rfl
73 
74 theorem polynomial_row_bound {n : ℕ} (E : Fin n → RealMatrix) (u : ℝ)
75     (hu : u∈Set.Icc (-1 : ℝ) 1) (v : ℂ) (hv : ‖v‖≤1) (i : Fin 3) :
76     |RationalBernsteinMargin.coordinate i
77       (PolynomialGram.operatorPolynomial (fun k => matrixOperator (E k)) u (1,v))|≤
78         ∑ k : Fin n,∑ j,|E k i j| := by
79   rw [polynomial_coordinate]
80   calc
81     _ ≤ ∑ k : Fin n,|u^(k : ℕ)*RationalBernsteinMargin.coordinate i (matrixOperator (E k) (1,v))| :=
82       Finset.abs_sum_le_sum_abs _ _
83     _ ≤ _ := by
84       apply Finset.sum_le_sum
85       intro k _
86       rw [abs_mul]
87       have hp : |u^(k : ℕ)|≤1 := by rw [abs_pow]; exact pow_le_one₀ (abs_nonneg _) (abs_le.mpr hu)
88       exact (mul_le_mul hp (row_bound (E k) v hv i) (abs_nonneg _) (by norm_num)).trans_eq (one_mul _)
89 
90 theorem polynomial_output_bounds {n : ℕ} (E : Fin n → RealMatrix) (r : Fin n → ℝ)
91     (hE : ∀ k i j,|E k i j|≤r k) (u : ℝ) (hu : u∈Set.Icc (-1 : ℝ) 1)
92     (v : ℂ) (hv : ‖v‖≤1) :
93     |(PolynomialGram.operatorPolynomial (fun k => matrixOperator (E k)) u (1,v)).1|≤3*∑ k,r k ∧
94     ‖(PolynomialGram.operatorPolynomial (fun k => matrixOperator (E k)) u (1,v)).2‖≤6*∑ k,r k := by
95   have hr (i : Fin 3) : (∑ k : Fin n,∑ j,|E k i j|)≤3*∑ k,r k := by
96     calc
97       _ ≤ ∑ k : Fin n,3*r k := Finset.sum_le_sum fun k _ => entry_row_bound (E k) (r k) (hE k) i
98       _ = _ := (Finset.mul_sum _ _ _).symm
99   have h0 := (polynomial_row_bound E u hu v hv 0).trans (hr 0)
100   have h1 := (polynomial_row_bound E u hu v hv 1).trans (hr 1)
101   have h2 := (polynomial_row_bound E u hu v hv 2).trans (hr 2)
102   refine ⟨h0,?_⟩
103   have hn := Complex.norm_le_abs_re_add_abs_im (PolynomialGram.operatorPolynomial (fun k => matrixOperator (E k)) u (1,v)).2
104   change |(PolynomialGram.operatorPolynomial (fun k => matrixOperator (E k)) u (1,v)).2.re|≤3*∑ k,r k at h1
105   change |(PolynomialGram.operatorPolynomial (fun k => matrixOperator (E k)) u (1,v)).2.im|≤3*∑ k,r k at h2
106   linarith
107 
108 end Komorebi.LSM.ComplexCoefficientBox

Back to source controls