CurvedMomentPolynomial.lean

1 import KomorebiLSM.CurvedMomentInstrument
2 import KomorebiLSM.PolynomialGram
3 import Mathlib.Tactic
4 
5 /-! Explicit degree-four coefficient matrices and reference-weighted moments. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.CurvedMoment
8 open MeasureTheory
9 open scoped Matrix BigOperators
10 noncomputable section
11 
12 def coefficientMatrix (a b : ℝ) : Fin 5 → Matrix (Fin 3) (Fin 3) ℝ :=
13   ![!![1,0,-b/2;0,0,0;0,0,0],
14     !![0,a,0;1,0,-b/2;0,0,0],
15     !![0,0,3*b/2;0,a,0;1,0,-b/2],
16     !![0,0,0;0,0,3*b/2;0,a,0],
17     !![0,0,0;0,0,0;0,0,3*b/2]]
18 
19 def coefficientOperator (a b : ℝ) (k : Fin 5) : State →L[ℝ] State :=
20   (coefficientMatrix a b k).mulVecLin.toContinuousLinearMap
21 
22 theorem branch_polynomial (a b u : ℝ) :
23     PolynomialGram.operatorPolynomial (coefficientOperator a b) u=branch a b u := by
24   ext z i
25   fin_cases i <;>
26     norm_num [PolynomialGram.operatorPolynomial,coefficientOperator,coefficientMatrix,
27       Fin.sum_univ_succ,Matrix.mulVec,dotProduct,branch_apply,likelihood,legendre,curve] <;> ring
28 
29 namespace Reference
30 variable {μ : Measure ℝ} (R : Reference μ)
31 include R
32 
33 theorem integral_polynomial (c : Fin 5 → ℝ) :
34     (∫ u,∑ k : Fin 5,c k*u^(k:ℕ)∂μ)=c 0+c 2/3+c 4/5 := by
35   let := R.probability
36   rw [integral_finsetSum (f:=fun (k:Fin 5) u => c k*u^(k:ℕ)) _ (fun k _ =>
37     (R.continuous_integrable (f:=fun u : ℝ => u^(k:ℕ)) (by fun_prop)).const_mul (c k))]
38   simp only [integral_const_mul]
39   norm_num [Fin.sum_univ_succ,R.first,R.second,R.third,R.fourth]
40   change c 0+(c 2*(1/3)+c 4*(1/5))=c 0+c 2/3+c 4/5
41   ring
42 
43 theorem integral_signal_likelihood (a b : ℝ) (z : State) :
44     (∫ u,u*likelihood a b u z∂μ)=a*z 1/3 := by
45   have he : (fun u => u*likelihood a b u z)=
46       (fun u => ∑ k : Fin 5,(![0,z 0-b*z 2/2,a*z 1,3*b*z 2/2,0] k)*u^(k:ℕ)) := by
47     funext u
48     norm_num [Fin.sum_univ_succ,likelihood,legendre]
49     ring
50   rw [he,R.integral_polynomial]
51   change 0+(a*z 1)/3+0/5=a*z 1/3
52   ring
53 
54 theorem integral_legendre_likelihood (a b : ℝ) (z : State) :
55     (∫ u,legendre u*likelihood a b u z∂μ)=b*z 2/5 := by
56   have he : (fun u => legendre u*likelihood a b u z)=
57       (fun u => ∑ k : Fin 5,(![-z 0/2+b*z 2/4,-a*z 1/2,
58         3*z 0/2-3*b*z 2/2,3*a*z 1/2,9*b*z 2/4] k)*u^(k:ℕ)) := by
59     funext u
60     norm_num [Fin.sum_univ_succ,likelihood,legendre]
61     ring
62   rw [he,R.integral_polynomial]
63   change (-z 0/2+b*z 2/4)+(3*z 0/2-3*b*z 2/2)/3+(9*b*z 2/4)/5=b*z 2/5
64   ring
65 
66 end Reference
67 end
68 end Komorebi.LSM.CurvedMoment

Back to source controls