BaseNormIntegration.lean

1 import KomorebiLSM.BaseNormTopology
2 import Mathlib.Analysis.Convex.Integral
3 import Mathlib.Analysis.LocallyConvex.WithSeminorms
4 
5 /-! Measurability and integration of the actual positive-decomposition infimum. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.BaseNorm.ProbabilityCone
8 open MeasureTheory
9 open scoped BigOperators NNReal
10 variable {E X : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
11 variable [FiniteDimensional ℝ E] (C : ProbabilityCone E)
12 
13 /-- Finite coordinates bound the actual infimum by the ambient norm. -/
14 theorem value_le_const_mul_norm : ∃ K > 0,∀ x : E,C.value x≤K*‖x‖ := by
15   let b := Module.finBasis ℝ E
16   let K := ∑ i,‖(b.coord i).toContinuousLinearMap‖ * C.value (b i)
17   have hK : 0≤K := Finset.sum_nonneg (fun i _ => mul_nonneg (norm_nonneg _) (C.value_nonneg _))
18   refine ⟨K+1,by linarith,?_⟩
19   intro x
20   have hsum : C.value x≤∑ i,|(b.repr x) i| * C.value (b i) := by
21     convert C.value_sum_le Finset.univ (fun i => (b.repr x) i • b i) using 1
22     · rw [b.sum_repr]
23     · simp only [C.value_smul]
24   calc C.value x ≤ ∑ i,|(b.repr x) i| * C.value (b i) := hsum
25     _ ≤ ∑ i,(‖(b.coord i).toContinuousLinearMap‖ * ‖x‖) * C.value (b i) := by
26       apply Finset.sum_le_sum
27       intro i _
28       apply mul_le_mul_of_nonneg_right _ (C.value_nonneg _)
29       exact (b.coord i).toContinuousLinearMap.le_opNorm x
30     _ = K*‖x‖ := by simp only [K,Finset.sum_mul]; apply Finset.sum_congr rfl; intro i _; ring
31     _ ≤ (K+1)*‖x‖ := by nlinarith [norm_nonneg x]
32 
33 theorem value_continuous : Continuous C.value := by
34   obtain ⟨K,hK,hbound⟩ := C.value_le_const_mul_norm
35   let q : Seminorm ℝ E := K.toNNReal • normSeminorm ℝ E
36   have hq : Continuous (q : E → ℝ) := by
37     change Continuous (fun x : E => (K.toNNReal : ℝ)*‖x‖)
38     exact continuous_const.mul continuous_norm
39   change Continuous (C.seminorm : E → ℝ)
40   apply Seminorm.continuous_of_le hq
41   intro x
42   change C.value x≤(K.toNNReal : ℝ)*‖x‖
43   simpa only [Real.coe_toNNReal K hK.le] using hbound x
44 
45 variable [MeasurableSpace X] {μ : Measure X}
46 
47 theorem integrable_value {f : X → E} (hf : Integrable f μ) :
48     Integrable (fun x => C.value (f x)) μ := by
49   obtain ⟨K,_,hK⟩ := C.value_le_const_mul_norm
50   apply (hf.norm.const_mul K).mono' (C.value_continuous.comp_aestronglyMeasurable hf.aestronglyMeasurable)
51   filter_upwards [] with x
52   rw [Real.norm_eq_abs,abs_of_nonneg (C.value_nonneg _)]
53   exact hK (f x)
54 
55 theorem value_integral_le_integral_value_probability [IsProbabilityMeasure μ] {f : X → E}
56     (hf : Integrable f μ) : C.value (∫ x,f x∂μ)≤∫ x,C.value (f x)∂μ := by
57   exact C.seminorm.convexOn.map_integral_le C.value_continuous.continuousOn isClosed_univ
58     (Filter.Eventually.of_forall (fun _ => Set.mem_univ _)) hf (C.integrable_value hf)
59 
60 
61 /-- The same integral inequality holds on finite restrictions and weighted cells. -/
62 theorem value_integral_le_integral_value [IsFiniteMeasure μ] {f : X → E}
63     (hf : Integrable f μ) : C.value (∫ x,f x∂μ)≤∫ x,C.value (f x)∂μ := by
64   by_cases hμ : μ=0
65   · simp [hμ]
66   · have : NeZero μ := ⟨hμ⟩
67     have h := C.seminorm.convexOn.map_average_le C.value_continuous.continuousOn isClosed_univ
68       (Filter.Eventually.of_forall (fun _ => Set.mem_univ _)) hf (C.integrable_value hf)
69     change C.value (average μ f)≤average μ (fun x => C.value (f x)) at h
70     rw [average_eq,average_eq,C.value_smul,abs_of_nonneg (inv_nonneg.mpr (measureReal_nonneg)),
71       smul_eq_mul] at h
72     exact (mul_le_mul_iff_right₀ (inv_pos.mpr measureReal_univ_pos)).mp h
73 
74 end Komorebi.LSM.BaseNorm.ProbabilityCone

Back to source controls