PositiveCellP58.lean

1 import KomorebiLSM.PositiveCellUniform
2 
3 /-! Full P58 endpoints on the actual averaged continuous instrument. -/
4 set_option autoImplicit false
5 namespace Komorebi.LSM.PositiveCellApproximation
6 open MeasureTheory ProbabilityTheory ContinuousInstrument ContinuousBins
7 variable {E A Y I : Type*} [Fintype I]
8 variable [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
9 variable [MeasurableSpace E] [BorelSpace E]
10 variable [MeasurableSpace Y] [PseudoMetricSpace Y] [BorelSpace Y]
11 variable {C : BaseNorm.ProbabilityCone E} {μ : Measure Y} [IsProbabilityMeasure μ]
12 
13 /-- P58: the actual normalized Bochner cell averages preserve the cone and
14 mass, retain every exact event-cell operator, and satisfy the displayed
15 supremum discrepancy bound in the genuine induced base norm. -/
16 theorem positive_cell_average_certificate
17     (D : DensityInstrument (A := A) C μ) (P : CellPartition μ I)
18     (L h : ℝ) (hL : 0≤L) (hh : 0≤h)
19     (hl : CellLipschitz D P L) (hd : CellDiameter P h) :
20     let K := instrument D P
21     (∀ a y z,z∈C.carrier → K.op a y z∈C.carrier) ∧
22     (∀ a z,C.mass ((∫ y,K.op a y∂μ) z)=C.mass z) ∧
23     (∀ a i,cellOperator μ (K.op a) (P.cell i)=cellOperator μ (D.op a) (P.cell i)) ∧
24     (∀ a,IsMarkovKernel (K.kernel a)) ∧ approximationError D P≤L*h := by
25   dsimp only
26   refine ⟨?_,(instrument D P).mass_preserving,?_,?_,approximationError_le_diameter D P hL hh hl hd⟩
27   · exact fun a y z hz => operator_positive D P a y hz
28   · exact exact_cell_operator D P
29   · intro a
30     infer_instance
31 
32 omit [MeasurableSpace Y] [PseudoMetricSpace Y] [BorelSpace Y] [IsProbabilityMeasure μ] in
33 /-- The same actual positive approximation has the sharper uniform equal-cell
34 error Lh/3; positivity and exact normalization are retained together with it. -/
35 theorem positive_equal_interval_certificate
36     (D : DensityInstrument (A := A) C UniformIntervalMoments.measure)
37     (P : CellPartition UniformIntervalMoments.measure I)
38     (a b : I → ℝ) (L h : ℝ) (hL : 0≤L) (hh : 0<h)
39     (hc : ∀ i,P.cell i=Set.Ioc (a i) (b i))
40     (ha : ∀ i,-1≤a i) (hb : ∀ i,b i≤1) (hw : ∀ i,b i-a i=h)
41     (hl : ∀ act,∀ y∈Set.Icc (-1 : ℝ) 1,∀ v∈Set.Icc (-1 : ℝ) 1,
42       inducedNorm (C := C) (D.op act y-D.op act v)≤L*dist y v) :
43     let K := instrument D P
44     (∀ act y z,z∈C.carrier → K.op act y z∈C.carrier) ∧
45     (∀ act z,C.mass ((∫ y,K.op act y∂UniformIntervalMoments.measure) z)=C.mass z) ∧
46     (∀ act i,cellOperator UniformIntervalMoments.measure (K.op act) (P.cell i)=
47       cellOperator UniformIntervalMoments.measure (D.op act) (P.cell i)) ∧
48     (∀ act,IsMarkovKernel (K.kernel act)) ∧ approximationError D P≤L*h/3 := by
49   dsimp only
50   refine ⟨?_,(instrument D P).mass_preserving,?_,?_,
51     approximationError_le_equal_intervals P D a b h L hh hL hc ha hb hw hl⟩
52   · exact fun act y z hz => operator_positive D P act y hz
53   · exact exact_cell_operator D P
54   · intro act
55     infer_instance
56 
57 end Komorebi.LSM.PositiveCellApproximation

Back to source controls