ObservableMomentBoundaries.lean

1 import KomorebiLSM.ObservableMomentConfidence
2 import KomorebiLSM.BaseNormModels
3 
4 /-! Actual instrument, basis and weighted-norm boundaries for P82. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.ObservableMoments.Boundaries
7 open MeasureTheory Matrix RegressionConfidence
8 open scoped BigOperators Matrix
9 
10 abbrev Vec2 := Fin 2 → ℝ
11 noncomputable def simplexCone : BaseNorm.ProbabilityCone Vec2 := BaseNorm.orthant (Fin 2)
12 noncomputable def onePointReference : Measure Unit := Measure.dirac ()
13 instance onePointReference_probability : IsProbabilityMeasure onePointReference := by
14   unfold onePointReference
15   infer_instance
16 
17 noncomputable def identityInstrument :
18     ContinuousInstrument.DensityInstrument (A := Unit) simplexCone onePointReference where
19   op _ _ := ContinuousLinearMap.id ℝ Vec2
20   measurable_op _ := measurable_const
21   integrable_op _ := integrable_const _
22   positive _ := Filter.Eventually.of_forall (fun _ _ hz => hz)
23   mass_preserving _ z := by
24     rw [integral_const,probReal_univ,one_smul]
25     rfl
26 
27 noncomputable def leftState : ContinuousInstrument.DensityInstrument.State simplexCone :=
28   ⟨![1,0],by
29     constructor
30     · rw [simplexCone,BaseNorm.orthant_carrier]
31       intro i
32       fin_cases i <;> norm_num
33     · change (∑ i : Fin 2,![1,0] i)=1
34       norm_num [Fin.sum_univ_two]⟩
35 
36 noncomputable def rightState : ContinuousInstrument.DensityInstrument.State simplexCone :=
37   ⟨![0,1],by
38     constructor
39     · rw [simplexCone,BaseNorm.orthant_carrier]
40       intro i
41       fin_cases i <;> norm_num
42     · change (∑ i : Fin 2,![0,1] i)=1
43       norm_num [Fin.sum_univ_two]⟩
44 
45 theorem identity_moment (z : Vec2) : momentOperator identityInstrument (fun _ : Unit => 1) () z=z := by
46   change (∫ _ : Unit,(1:ℝ) • ContinuousLinearMap.id ℝ Vec2∂onePointReference) z=z
47   rw [one_smul,integral_const,probReal_univ,one_smul]
48   rfl
49 
50 theorem wrong_posterior_mean :
51     (∫ _ : Unit,rightState.1∂identityInstrument.kernel () leftState)=rightState.1 := by
52   rw [integral_const,probReal_univ,one_smul]
53 
54 theorem wrong_accessible_posterior_not_mean :
55     (∫ _ : Unit,rightState.1∂identityInstrument.kernel () leftState)≠
56       momentOperator identityInstrument (fun _ : Unit => 1) () leftState.1 := by
57   rw [wrong_posterior_mean,identity_moment]
58   intro he
59   have h0 := congrFun he 0
60   norm_num [leftState,rightState] at h0
61 
62 noncomputable def firstCoefficients (k : Fin 2) : Vec2 →L[ℝ] Vec2 :=
63   if k=0 then ContinuousLinearMap.id ℝ Vec2 else 0
64 noncomputable def secondCoefficients (k : Fin 2) : Vec2 →L[ℝ] Vec2 :=
65   if k=1 then ContinuousLinearMap.id ℝ Vec2 else 0
66 
67 def repeatedBasis (_ : Fin 2) (_ : Unit) : ℝ := 1
68 
69 theorem first_expansion (u : Unit) : identityInstrument.op () u=
70     ∑ k : Fin 2,repeatedBasis k u • firstCoefficients k := by
71   simp [identityInstrument,repeatedBasis,firstCoefficients]
72 
73 theorem second_expansion (u : Unit) : identityInstrument.op () u=
74     ∑ k : Fin 2,repeatedBasis k u • secondCoefficients k := by
75   simp [identityInstrument,repeatedBasis,secondCoefficients]
76 
77 theorem coefficients_distinct : firstCoefficients≠secondCoefficients := by
78   intro he
79   have h0 := congrArg (fun F : Fin 2 → Vec2 →L[ℝ] Vec2 => F 0 leftState.1 0) he
80   norm_num [firstCoefficients,secondCoefficients,leftState] at h0
81 
82 theorem repeated_moment_matrix :
83     basisMomentMatrix (ν := onePointReference) repeatedBasis repeatedBasis=!![1,1;1,1] := by
84   ext i j
85   fin_cases i <;> fin_cases j <;>
86     simp [basisMomentMatrix,repeatedBasis]
87 
88 theorem repeated_moment_matrix_singular :
89     ¬IsUnit (basisMomentMatrix (ν := onePointReference) repeatedBasis repeatedBasis) := by
90   rw [repeated_moment_matrix,Matrix.isUnit_iff_isUnit_det]
91   norm_num [Matrix.det_fin_two]
92 
93 noncomputable def smallDesign : Matrix (Fin 1) (Fin 1) ℝ := (1/4:ℝ) • 1
94 def unitDirection : Fin 1 → ℝ := fun _ => 1
95 
96 theorem smallDesign_posDef : smallDesign.PosDef := Matrix.PosDef.one.smul (by norm_num)
97 
98 theorem small_weighted_norm : weightedNorm smallDesign unitDirection=1/2 := by
99   norm_num [weightedNorm,smallDesign,unitDirection,Matrix.mulVec,dotProduct,Fin.sum_univ_one]
100 
101 theorem unit_direction_pairing : |unitDirection ⬝ᵥ unitDirection|=1 := by
102   norm_num [unitDirection,dotProduct,Fin.sum_univ_one]
103 
104 end Komorebi.LSM.ObservableMoments.Boundaries

Back to source controls