Section88ComparisonBudget.lean

1 import KomorebiLSM.Section88Reference
2 import KomorebiLSM.RationalLorentzAlgebra
3 import KomorebiLSM.ComplexCoefficientBox
4 import KomorebiLSM.UniformAbsoluteMoments
5 
6 /-! Exact row-sum coefficient bounds and their genuine normalized integrated budget. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.Section88ComparisonBudget
9 open scoped BigOperators
10 open LorentzCylinder RationalBernsteinMargin RationalLorentzMatrix PerturbedOperatorFixture
11 open MeasureTheory ContinuousInstrument UniformIntervalMoments
12 noncomputable section
13 
14 def errorMatrix (a : Bool) (k : Fin 3) : RationalMatrix := rawComparison a k-referenceComparison a k
15 
16 def coefficientBound (k : Fin 3) : ℝ := ![11/5000,137/30000,37/8000] k
17 
18 set_option backward.isDefEq.respectTransparency false in
19 theorem coefficient_error (a : Bool) (k : Fin 3) (v : ℂ) (hv : ‖v‖≤1) :
20     probabilityCone.value (matrixOperator (errorMatrix a k) (1,v))≤coefficientBound k := by
21   have h := ComplexCoefficientBox.value_bound (fun i j => (errorMatrix a k i j : ℝ)) v hv
22   rw [ComplexCoefficientBox.matrixOperator_rat] at h
23   apply h.trans
24   simp only [errorMatrix,Matrix.sub_apply,Rat.cast_sub]
25   have hk : k=0 ∨ k=1 ∨ k=2 := by omega
26   rcases hk with hk | hk | hk <;> subst k <;> cases a <;>
27     norm_num [coefficientBound,Fin.sum_univ_succ,Matrix.cons_val_two]
28 
29 def rawOperator (a : Bool) (u : ℝ) : State ℂ →L[ℝ] State ℂ :=
30   PolynomialGram.operatorPolynomial (fun k => matrixOperator (rawComparison a k)) u
31 
32 theorem raw_difference (a : Bool) (u : ℝ) (z : State ℂ) :
33     rawOperator a u z-Section88Reference.operator a u z=
34       ∑ k : Fin 3,u^(k : ℕ) • matrixOperator (errorMatrix a k) z := by
35   simp only [rawOperator,Section88Reference.operator,PolynomialGram.operatorPolynomial,
36     errorMatrix,matrixOperator_sub,sub_apply,sum_apply,smul_apply,smul_sub,
37     Finset.sum_sub_distrib]
38 
39 theorem pointwise_raw_error (a : Bool) (u : ℝ) (v : ℂ) (hv : ‖v‖≤1) :
40     probabilityCone.value (rawOperator a u (1,v)-Section88Reference.operator a u (1,v))≤
41       ∑ k : Fin 3,|u|^(k : ℕ)*coefficientBound k := by
42   rw [raw_difference]
43   apply (probabilityCone.value_sum_le _ _).trans
44   apply Finset.sum_le_sum
45   intro k _
46   rw [probabilityCone.value_smul,abs_pow]
47   exact mul_le_mul_of_nonneg_left (coefficient_error a k v hv) (pow_nonneg (abs_nonneg _) _)
48 
49 theorem mass_matrix_of_row (M : RationalMatrix) (q : ℚ)
50     (h : ∀ j,M 0 j=if j=0 then q else 0) (z : State ℂ) :
51     coordinate 0 (matrixOperator M z)=(q : ℝ)*z.1 := by
52   rw [coordinate_matrixOperator]
53   simp_rw [h]
54   norm_num [Fin.sum_univ_succ,coordinate,Matrix.cons_val_two]
55 
56 theorem moment_mass_of_rows (M : Fin 3 → RationalMatrix) (q0 q2 : ℚ)
57     (h0 : ∀ j,M 0 0 j=if j=0 then q0 else 0)
58     (h2 : ∀ j,M 2 0 j=if j=0 then q2 else 0) (hq : q0+q2/3=1) (z : State ℂ) :
59     probabilityCone.mass ((∑ k : Fin 3,moment k • matrixOperator (M k)) z)=probabilityCone.mass z := by
60   have hc0 := mass_matrix_of_row (M 0) q0 h0 z
61   have hc2 := mass_matrix_of_row (M 2) q2 h2 z
62   change coordinate 0 ((∑ k : Fin 3,moment k • matrixOperator (M k)) z)=z.1
63   simp only [sum_apply,smul_apply,map_sum,map_smul]
64   simp only [Fin.sum_univ_succ]
65   change moment 0*coordinate 0 (matrixOperator (M 0) z)+
66     (moment 1*coordinate 0 (matrixOperator (M 1) z)+
67       (moment 2*coordinate 0 (matrixOperator (M 2) z)+0))=z.1
68   have hms : moment 0=1 ∧ moment 1=0 ∧ moment 2=1/3 := by norm_num [moment_formula]
69   rw [hms.1,hms.2.1,hms.2.2,hc0,hc2]
70   simp only [one_mul,zero_mul,add_zero,zero_add]
71   have hqr : (q0 : ℝ)+(q2 : ℝ)/3=1 := by exact_mod_cast hq
72   calc
73     _=((q0 : ℝ)+(q2 : ℝ)/3)*z.1 := by ring
74     _=z.1 := by rw [hqr]; ring
75 
76 theorem raw_moment_mass (a : Bool) (z : State ℂ) :
77     probabilityCone.mass ((∑ k : Fin 3,moment k • matrixOperator (rawComparison a k)) z)=probabilityCone.mass z := by
78   apply moment_mass_of_rows (rawComparison a) (1/4) (9/4) _ _ (by norm_num) z
79   · intro j
80     cases a <;> fin_cases j <;> norm_num [Matrix.cons_val_two]
81   · intro j
82     cases a <;> fin_cases j <;> norm_num [Matrix.cons_val_two]
83 
84 def rawEstimate : InteriorRepair.EstimateFamily (V := ℂ) (A := Bool) :=
85   InteriorRepair.EstimateFamily.ofPolynomial (fun a k => matrixOperator (rawComparison a k)) raw_moment_mass
86 
87 /-- No signed odd-moment cancellation is used for this error integral. -/
88 theorem integrated_raw_error (a : Bool) (z : State ℂ) (hz : z∈probabilityCone.base) :
89     (∫ u,probabilityCone.value (rawEstimate.op a u z-Section88Reference.instrument.op a u z)∂measure)≤241/40000 := by
90   have hm : z.1=1 := hz.2
91   have hv : ‖z.2‖≤1 := by rw [← hm]; exact hz.1
92   have he : z=(1,z.2) := Prod.ext hm rfl
93   have hi := probabilityCone.integrable_value
94     ((rawEstimate.applied_integrable a z).sub (Section88Reference.instrument.applied_integrable a z))
95   have hj : Integrable (fun u => ∑ k : Fin 3,|u|^(k : ℕ)*coefficientBound k) measure := by
96     exact integrable_finsetSum _ (fun k _ => (UniformAbsoluteMoments.abs_power_integrable k).mul_const _)
97   have hp (u : ℝ) : probabilityCone.value (rawEstimate.op a u z-Section88Reference.instrument.op a u z)≤
98       ∑ k : Fin 3,|u|^(k : ℕ)*coefficientBound k := by
99     rw [he]
100     exact pointwise_raw_error a u z.2 hv
101   apply (integral_mono hi hj hp).trans
102   rw [integral_finsetSum Finset.univ (fun (k : Fin 3) _ => (UniformAbsoluteMoments.abs_power_integrable k).mul_const _)]
103   simp_rw [integral_mul_const,UniformAbsoluteMoments.integral_abs_power]
104   norm_num [coefficientBound,Fin.sum_univ_succ,Matrix.cons_val_two]
105 
106 end
107 end Komorebi.LSM.Section88ComparisonBudget

Back to source controls