RationalBernsteinMargin.lean

1 import KomorebiLSM.RationalSemicircle
2 import KomorebiLSM.TensorBernsteinCertificate
3 
4 /-! The submitted rational tensor polynomials are the literal operator chart tests. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.RationalBernsteinMargin
7 open scoped BigOperators
8 open LorentzCylinder RobustOrientedMargin RationalSemicircle TensorBernsteinCertificate
9 noncomputable section
10 
11 abbrev RationalMatrix := Matrix (Fin 3) (Fin 3) ℚ
12 
13 def coordinate : Fin 3 → State ℂ →L[ℝ] ℝ :=
14   ![ContinuousLinearMap.fst ℝ ℝ ℂ,
15     Complex.reCLM.comp (ContinuousLinearMap.snd ℝ ℝ ℂ),
16     Complex.imCLM.comp (ContinuousLinearMap.snd ℝ ℝ ℂ)]
17 
18 def row (M : RationalMatrix) (i : Fin 3) : State ℂ →L[ℝ] ℝ :=
19   ∑ j,(M i j : ℝ) • coordinate j
20 
21 /-- A rational three-coordinate matrix acting on the actual mass/spatial state space. -/
22 def matrixOperator (M : RationalMatrix) : State ℂ →L[ℝ] State ℂ :=
23   (row M 0).prod (Complex.equivRealProdCLM.symm.toContinuousLinearMap.comp
24     ((row M 1).prod (row M 2)))
25 
26 @[simp] theorem coordinate_matrixOperator (M : RationalMatrix) (i : Fin 3) (z : State ℂ) :
27     coordinate i (matrixOperator M z)=∑ j,(M i j : ℝ)*coordinate j z := by
28   fin_cases i <;> simp [coordinate,matrixOperator,row]
29 
30 def denominatorPolynomial : Polynomial₂ := 1+MvPolynomial.X 1^2
31 
32 def liftPolynomial (left : Bool) : Fin 3 → Polynomial₂ :=
33   ![denominatorPolynomial,
34     (if left then -1 else 1)*(1-MvPolynomial.X 1^2),
35     (if left then -1 else 1)*(2*MvPolynomial.X 1)]
36 
37 theorem value_liftPolynomial (left : Bool) (i : Fin 3) (u t : ℝ) :
38     value (liftPolynomial left i) ![u,t]=coordinate i (lift left t) := by
39   fin_cases i <;> cases left <;>
40     simp [liftPolynomial,denominatorPolynomial,value,coordinate,lift,numerator,denominator]
41 
42 variable {n : ℕ}
43 
44 def outputPolynomial (G : Fin n → RationalMatrix) (left : Bool) (i : Fin 3) : Polynomial₂ :=
45   ∑ k,∑ j,MvPolynomial.C (G k i j)*MvPolynomial.X 0^(k : ℕ)*liftPolynomial left j
46 
47 /-- Polynomial equality is connected to the complete operator family, not interpolation samples. -/
48 theorem value_outputPolynomial (G : Fin n → RationalMatrix) (left : Bool) (i : Fin 3) (u t : ℝ) :
49     value (outputPolynomial G left i) ![u,t]=
50       coordinate i (PolynomialGram.operatorPolynomial (fun k => matrixOperator (G k)) u (lift left t)) := by
51   simp only [outputPolynomial,value,MvPolynomial.eval₂_sum,map_sum,map_smul,
52     sum_apply,smul_apply,
53     PolynomialGram.operatorPolynomial,coordinate_matrixOperator]
54   simp only [MvPolynomial.eval₂_mul,MvPolynomial.eval₂_C,MvPolynomial.eval₂_pow,
55     MvPolynomial.eval₂_X,Matrix.cons_val_zero]
56   change (∑ k : Fin n,∑ j : Fin 3,((G k i j : ℝ)*u^(k : ℕ))*value (liftPolynomial left j) ![u,t])=
57     ∑ k : Fin n,u^(k : ℕ)*(∑ j : Fin 3,(G k i j : ℝ)*coordinate j (lift left t))
58   simp only [value_liftPolynomial,Finset.mul_sum]
59   congr 1
60   funext k
61   apply Finset.sum_congr rfl
62   intro j _
63   ring
64 
65 def orientationPolynomial (G : Fin n → RationalMatrix) (kappa : ℚ) (left : Bool) : Polynomial₂ :=
66   outputPolynomial G left 0-MvPolynomial.C kappa*denominatorPolynomial
67 
68 def squareGapPolynomial (G : Fin n → RationalMatrix) (kappa : ℚ) (left : Bool) : Polynomial₂ :=
69   orientationPolynomial G kappa left^2-outputPolynomial G left 1^2-outputPolynomial G left 2^2
70 
71 theorem value_orientationPolynomial (G : Fin n → RationalMatrix) (kappa : ℚ) (left : Bool) (u t : ℝ) :
72     value (orientationPolynomial G kappa left) ![u,t]=
73       orientation (PolynomialGram.operatorPolynomial (fun k => matrixOperator (G k)) u) kappa left t := by
74   rw [orientationPolynomial,value,MvPolynomial.eval₂_sub,MvPolynomial.eval₂_mul,
75     MvPolynomial.eval₂_C]
76   change value (outputPolynomial G left 0) ![u,t]-(kappa : ℝ)*value denominatorPolynomial ![u,t]=_
77   rw [value_outputPolynomial]
78   simp [coordinate,value,denominatorPolynomial,orientation,denominator]
79 
80 theorem value_squareGapPolynomial (G : Fin n → RationalMatrix) (kappa : ℚ) (left : Bool) (u t : ℝ) :
81     value (squareGapPolynomial G kappa left) ![u,t]=
82       squareGap (PolynomialGram.operatorPolynomial (fun k => matrixOperator (G k)) u) kappa left t := by
83   simp only [squareGapPolynomial,value,MvPolynomial.eval₂_sub,MvPolynomial.eval₂_pow]
84   change value (orientationPolynomial G kappa left) ![u,t]^2-
85     value (outputPolynomial G left 1) ![u,t]^2-value (outputPolynomial G left 2) ![u,t]^2=_
86   rw [value_orientationPolynomial,value_outputPolynomial,value_outputPolynomial]
87   simp [coordinate,squareGap]
88 
89 /-- Both finite subdivision trees are required for every chart. -/
90 structure Certificate (G : Fin n → RationalMatrix) (kappa : ℚ) where
91   orientationWitness : ∀ left,SubdivisionWitness (orientationPolynomial G kappa left) square
92   squareGapWitness : ∀ left,SubdivisionWitness (squareGapPolynomial G kappa left) square
93 
94 /-- Literal finite rational witnesses certify the actual minimum over every disk input. -/
95 theorem Certificate.margin {G : Fin n → RationalMatrix} {kappa : ℚ} (cert : Certificate G kappa)
96     (u : ℝ) (hu : u∈Set.Icc (-1 : ℝ) 1) :
97     (kappa : ℝ)≤sigma (PolynomialGram.operatorPolynomial (fun k => matrixOperator (G k)) u) := by
98   apply margin_of_charts
99   · intro left t ht
100     rw [← value_orientationPolynomial]
101     apply (cert.orientationWitness left).sound
102     rw [square_domain]
103     intro i
104     fin_cases i
105     · exact hu
106     · exact ht
107   · intro left t ht
108     rw [← value_squareGapPolynomial]
109     apply (cert.squareGapWitness left).sound
110     rw [square_domain]
111     intro i
112     fin_cases i
113     · exact hu
114     · exact ht
115 
116 /-- Strict actual margin makes both literal chart tests strictly positive. -/
117 theorem strict_chart_tests (F : State ℂ →L[ℝ] State ℂ) (kappa : ℝ)
118     (hmargin : kappa<sigma F) (left : Bool) (t : ℝ) :
119     0<orientation F kappa left t ∧ 0<squareGap F kappa left t := by
120   have hm : kappa<slack (F (1,chart left t)) :=
121     hmargin.trans_le (sigma_le F _ (chart_norm left t).le)
122   have hd := denominator_pos t
123   have he : (F (lift left t)).2=denominator t • (F (1,chart left t)).2 := by
124     rw [lift_eq,map_smul]
125     rfl
126   have hf : orientation F kappa left t=
127       denominator t*((F (1,chart left t)).1-kappa) := by
128     unfold orientation
129     rw [lift_eq,map_smul]
130     change denominator t*(F (1,chart left t)).1-kappa*denominator t=_
131     ring
132   have hn : ‖(F (lift left t)).2‖<orientation F kappa left t := by
133     rw [he,norm_smul,Real.norm_eq_abs,abs_of_pos hd,hf]
134     apply mul_lt_mul_of_pos_left _ hd
135     dsimp [slack] at hm
136     linarith
137   have hf0 : 0<orientation F kappa left t := (norm_nonneg _).trans_lt hn
138   refine ⟨hf0,?_⟩
139   have hs : ‖(F (lift left t)).2‖^2<(orientation F kappa left t)^2 :=
140     (sq_lt_sq₀ (norm_nonneg _) hf0.le).mpr hn
141   rw [← Complex.normSq_eq_norm_sq,Complex.normSq_apply] at hs
142   unfold squareGap
143   nlinarith
144 
145 /-- The checked margin supplies actual pointwise cone preservation at every interval value. -/
146 theorem Certificate.preserves {G : Fin n → RationalMatrix} {kappa : ℚ} (cert : Certificate G kappa)
147     (hkappa : 0≤kappa) (u : ℝ) (hu : u∈Set.Icc (-1 : ℝ) 1)
148     {z : State ℂ} (hz : z∈cone) :
149     PolynomialGram.operatorPolynomial (fun k => matrixOperator (G k)) u z∈cone := by
150   apply preserves_of_normalized _ _ hz
151   intro v hv
152   have hm := ((le_sigma_iff _ _).mp (cert.margin u hu)) v hv
153   have hk : (0 : ℝ)≤kappa := by exact_mod_cast hkappa
154   change ‖(PolynomialGram.operatorPolynomial (fun k => matrixOperator (G k)) u (1,v)).2‖≤_
155   dsimp [slack] at hm
156   linarith
157 
158 /-- Exact averaged mass remains a separate algebraic check on the submitted complete family. -/
159 def certifiedInstrument {A : Type*} (G : A → Fin n → RationalMatrix) (kappa : ℚ)
160     (cert : ∀ a,Certificate (G a) kappa) (hkappa : 0≤kappa)
161     (hm : ∀ a z,probabilityCone.mass
162       ((∑ k : Fin n,UniformIntervalMoments.moment k • matrixOperator (G a k)) z)=probabilityCone.mass z) :
163     ContinuousInstrument.DensityInstrument (A := A) (probabilityCone (V := ℂ)) UniformIntervalMoments.measure where
164   op a := PolynomialGram.operatorPolynomial (fun k => matrixOperator (G a k))
165   measurable_op a := (PolynomialGram.operatorPolynomial_continuous _).measurable
166   integrable_op a := PolynomialGram.operatorPolynomial_integrable _
167   positive a := by
168     filter_upwards [PolynomialGram.uniform_ae_interval] with u hu
169     exact fun z hz => (cert a).preserves hkappa u hu hz
170   mass_preserving a z := by
171     rw [PolynomialGram.operatorPolynomial_integral]
172     exact hm a z
173 
174 theorem certified_record_probability {A : Type*} [Fintype A] [MeasurableSpace A]
175     [MeasurableSingletonClass A] (G : A → Fin n → RationalMatrix) (kappa : ℚ)
176     (cert : ∀ a,Certificate (G a) kappa) (hkappa : 0≤kappa)
177     (hm : ∀ a z,probabilityCone.mass
178       ((∑ k : Fin n,UniformIntervalMoments.moment k • matrixOperator (G a k)) z)=probabilityCone.mass z)
179     (policy : ContinuousRecords.Policy (A := A) (Y := ℝ)) (z : State ℂ)
180     (hz : z∈probabilityCone.base) (horizon : ℕ) :
181     MeasureTheory.IsProbabilityMeasure (ContinuousRecords.recordLaw
182       (certifiedInstrument G kappa cert hkappa hm) policy z horizon) :=
183   ContinuousRecords.recordLaw_probability (certifiedInstrument G kappa cert hkappa hm)
184     policy ⟨z,hz⟩ horizon
185 
186 end
187 end Komorebi.LSM.RationalBernsteinMargin

Back to source controls