Skip to content

Commit 8b3fbc9

Browse files
mcdollmcdoll
committed
feat: Positivity extension for Bochner integral (#10661)
Inspired by #10538 add a positivity extension for Bochner integrals.
1 parent f2f4854 commit 8b3fbc9

File tree

14 files changed

+72
-51
lines changed

14 files changed

+72
-51
lines changed

‎Mathlib/Analysis/Convolution.lean‎

Lines changed: 8 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -308,10 +308,9 @@ theorem MeasureTheory.Integrable.convolution_integrand (hf : Integrable f ν) (h
308308
· simp only [integral_sub_right_eq_self (‖g ·‖)]
309309
exact (hf.norm.const_mul _).mul_const _
310310
· simp_rw [← integral_mul_left]
311-
rw [Real.norm_of_nonneg]
312-
· exact integral_mono_of_nonneg (eventually_of_forall fun t => norm_nonneg _)
313-
((hg.comp_sub_right t).norm.const_mul _) (eventually_of_forall fun t => L.le_opNorm₂ _ _)
314-
exact integral_nonneg fun x => norm_nonneg _
311+
rw [Real.norm_of_nonneg (by positivity)]
312+
exact integral_mono_of_nonneg (eventually_of_forall fun t => norm_nonneg _)
313+
((hg.comp_sub_right t).norm.const_mul _) (eventually_of_forall fun t => L.le_opNorm₂ _ _)
315314
#align measure_theory.integrable.convolution_integrand MeasureTheory.Integrable.convolution_integrand
316315

317316
theorem MeasureTheory.Integrable.ae_convolution_exists (hf : Integrable f ν) (hg : Integrable g μ) :
@@ -1000,12 +999,11 @@ theorem convolution_assoc (hL : ∀ (x : E) (y : E') (z : E''), L₂ (L x y) z =
1000999
refine' (hfgk.const_mul (‖L₃‖ * ‖L₄‖)).mono' h2_meas
10011000
(((quasiMeasurePreserving_sub_left_of_right_invariant ν x₀).ae hgk).mono fun t ht => _)
10021001
· simp_rw [convolution_def, mul_apply', mul_mul_mul_comm ‖L₃‖ ‖L₄‖, ← integral_mul_left]
1003-
rw [Real.norm_of_nonneg]
1004-
· refine' integral_mono_of_nonneg (eventually_of_forall fun t => norm_nonneg _)
1005-
((ht.const_mul _).const_mul _) (eventually_of_forall fun s => _)
1006-
simp only [← mul_assoc ‖L₄‖]
1007-
apply_rules [ContinuousLinearMap.le_of_opNorm₂_le_of_le, le_rfl]
1008-
exact integral_nonneg fun x => norm_nonneg _
1002+
rw [Real.norm_of_nonneg (by positivity)]
1003+
refine' integral_mono_of_nonneg (eventually_of_forall fun t => norm_nonneg _)
1004+
((ht.const_mul _).const_mul _) (eventually_of_forall fun s => _)
1005+
simp only [← mul_assoc ‖L₄‖]
1006+
apply_rules [ContinuousLinearMap.le_of_opNorm₂_le_of_le, le_rfl]
10091007
#align convolution_assoc convolution_assoc
10101008

10111009
end Assoc

‎Mathlib/Analysis/SpecialFunctions/Gaussian.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -261,8 +261,7 @@ theorem integral_gaussian (b : ℝ) : ∫ x : ℝ, exp (-b * x ^ 2) = sqrt (π /
261261
· exact div_nonpos_of_nonneg_of_nonpos pi_pos.le hb
262262
· simpa only [not_lt, integrable_exp_neg_mul_sq_iff] using hb
263263
-- Assume now `b > 0`. Then both sides are non-negative and their squares agree.
264-
refine' (sq_eq_sq _ (sqrt_nonneg _)).1 _
265-
· exact integral_nonneg fun x => (exp_pos _).le
264+
refine' (sq_eq_sq (by positivity) (by positivity)).1 _
266265
rw [← ofReal_inj, ofReal_pow, ← coe_algebraMap, IsROrC.algebraMap_eq_ofReal, ← integral_ofReal,
267266
sq_sqrt (div_pos pi_pos hb).le, ← IsROrC.algebraMap_eq_ofReal, coe_algebraMap, ofReal_div]
268267
convert integral_gaussian_sq_complex (by rwa [ofReal_re] : 0 < (b : ℂ).re) with _ x

‎Mathlib/MeasureTheory/Covering/Differentiation.lean‎

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -917,12 +917,8 @@ theorem ae_tendsto_average_norm_sub {f : α → E} (hf : LocallyIntegrable f μ)
917917
have A : IntegrableOn (fun y => (‖f y - f x‖₊ : ℝ)) a μ := by
918918
simp_rw [coe_nnnorm]
919919
exact (h''a.sub (integrableOn_const.2 (Or.inr h'a))).norm
920-
rw [lintegral_coe_eq_integral _ A, ENNReal.toReal_ofReal]
921-
· simp_rw [coe_nnnorm]
922-
rfl
923-
· apply integral_nonneg
924-
intro x
925-
exact NNReal.coe_nonneg _
920+
rw [lintegral_coe_eq_integral _ A, ENNReal.toReal_ofReal (by positivity)]
921+
rfl
926922

927923
/-- *Lebesgue differentiation theorem*: for almost every point `x`, the
928924
average of `f` on `a` tends to `f x` as `a` shrinks to `x` along a Vitali family.-/

‎Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -127,8 +127,7 @@ theorem condexpIndL1Fin_smul' [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (hs
127127

128128
theorem norm_condexpIndL1Fin_le (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : G) :
129129
‖condexpIndL1Fin hm hs hμs x‖ ≤ (μ s).toReal * ‖x‖ := by
130-
have : 0 ≤ ∫ a : α, ‖condexpIndL1Fin hm hs hμs x a‖ ∂μ :=
131-
integral_nonneg fun a => norm_nonneg _
130+
have : 0 ≤ ∫ a : α, ‖condexpIndL1Fin hm hs hμs x a‖ ∂μ := by positivity
132131
rw [L1.norm_eq_integral_norm, ← ENNReal.toReal_ofReal (norm_nonneg x), ← ENNReal.toReal_mul, ←
133132
ENNReal.toReal_ofReal this,
134133
ENNReal.toReal_le_toReal ENNReal.ofReal_ne_top (ENNReal.mul_ne_top hμs ENNReal.ofReal_ne_top),

‎Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -93,12 +93,12 @@ theorem integral_abs_condexp_le (f : α → ℝ) : ∫ x, |(μ[f|m]) x| ∂μ
9393
by_cases hm : m ≤ m0
9494
swap
9595
· simp_rw [condexp_of_not_le hm, Pi.zero_apply, abs_zero, integral_zero]
96-
exact integral_nonneg fun x => abs_nonneg _
96+
positivity
9797
by_cases hfint : Integrable f μ
9898
swap
9999
· simp only [condexp_undef hfint, Pi.zero_apply, abs_zero, integral_const, Algebra.id.smul_eq_mul,
100100
mul_zero]
101-
exact integral_nonneg fun x => abs_nonneg _
101+
positivity
102102
rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
103103
· rw [ENNReal.toReal_le_toReal] <;> simp_rw [← Real.norm_eq_abs, ofReal_norm_eq_coe_nnnorm]
104104
· rw [← snorm_one_eq_lintegral_nnnorm, ← snorm_one_eq_lintegral_nnnorm]
@@ -118,12 +118,12 @@ theorem set_integral_abs_condexp_le {s : Set α} (hs : MeasurableSet[m] s) (f :
118118
by_cases hnm : m ≤ m0
119119
swap
120120
· simp_rw [condexp_of_not_le hnm, Pi.zero_apply, abs_zero, integral_zero]
121-
exact integral_nonneg fun x => abs_nonneg _
121+
positivity
122122
by_cases hfint : Integrable f μ
123123
swap
124124
· simp only [condexp_undef hfint, Pi.zero_apply, abs_zero, integral_const, Algebra.id.smul_eq_mul,
125125
mul_zero]
126-
exact integral_nonneg fun x => abs_nonneg _
126+
positivity
127127
have : ∫ x in s, |(μ[f|m]) x| ∂μ = ∫ x, |(μ[s.indicator f|m]) x| ∂μ := by
128128
rw [← integral_indicator (hnm _ hs)]
129129
refine' integral_congr_ae _

‎Mathlib/MeasureTheory/Function/ConditionalExpectation/Unique.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -208,7 +208,7 @@ theorem lintegral_nnnorm_le_of_forall_fin_meas_integral_eq (hm : m ≤ m0) {f g
208208
rw [← ofReal_integral_norm_eq_lintegral_nnnorm hfi, ←
209209
ofReal_integral_norm_eq_lintegral_nnnorm hgi, ENNReal.ofReal_le_ofReal_iff]
210210
· exact integral_norm_le_of_forall_fin_meas_integral_eq hm hf hfi hg hgi hgf hs hμs
211-
· exact integral_nonneg fun x => norm_nonneg _
211+
· positivity
212212
#align measure_theory.lintegral_nnnorm_le_of_forall_fin_meas_integral_eq MeasureTheory.lintegral_nnnorm_le_of_forall_fin_meas_integral_eq
213213

214214
end IntegralNormLE

‎Mathlib/MeasureTheory/Function/ContinuousMapDense.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -207,7 +207,7 @@ theorem Memℒp.exists_hasCompactSupport_integral_rpow_sub_le
207207
rwa [(hf.sub g_mem).snorm_eq_integral_rpow_norm B ENNReal.coe_ne_top,
208208
ENNReal.ofReal_le_ofReal_iff I.le, one_div, ENNReal.toReal_ofReal hp.le,
209209
Real.rpow_le_rpow_iff _ hε.le (inv_pos.2 hp)] at hg
210-
exact integral_nonneg fun x => Real.rpow_nonneg (norm_nonneg _) _
210+
positivity
211211
#align measure_theory.mem_ℒp.exists_has_compact_support_integral_rpow_sub_le MeasureTheory.Memℒp.exists_hasCompactSupport_integral_rpow_sub_le
212212

213213
/-- In a locally compact space, any integrable function can be approximated by compactly supported
@@ -300,7 +300,7 @@ theorem Memℒp.exists_boundedContinuous_integral_rpow_sub_le [μ.WeaklyRegular]
300300
rwa [(hf.sub g_mem).snorm_eq_integral_rpow_norm B ENNReal.coe_ne_top,
301301
ENNReal.ofReal_le_ofReal_iff I.le, one_div, ENNReal.toReal_ofReal hp.le,
302302
Real.rpow_le_rpow_iff _ hε.le (inv_pos.2 hp)] at hg
303-
exact integral_nonneg fun x => Real.rpow_nonneg (norm_nonneg _) _
303+
positivity
304304
#align measure_theory.mem_ℒp.exists_bounded_continuous_integral_rpow_sub_le MeasureTheory.Memℒp.exists_boundedContinuous_integral_rpow_sub_le
305305

306306
/-- Any integrable function can be approximated by bounded continuous functions,

‎Mathlib/MeasureTheory/Integral/Bochner.lean‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2079,3 +2079,26 @@ theorem snorm_one_le_of_le' {r : ℝ} {f : α → ℝ} (hfint : Integrable f μ)
20792079
end SnormBound
20802080

20812081
end MeasureTheory
2082+
2083+
namespace Mathlib.Meta.Positivity
2084+
2085+
open Qq Lean Meta MeasureTheory
2086+
2087+
/-- Positivity extension for integrals.
2088+
2089+
This extension only proves non-negativity, strict positivity is more delicate for integration and
2090+
requires more assumptions. -/
2091+
@[positivity MeasureTheory.integral _ _]
2092+
def evalIntegral : PositivityExt where eval {u α} zα pα e := do
2093+
match u, α, e with
2094+
| 0, ~q(ℝ), ~q(@MeasureTheory.integral $i ℝ _ $inst2 _ _ $f) =>
2095+
let i : Q($i) ← mkFreshExprMVarQ q($i) .syntheticOpaque
2096+
have body : Q(ℝ) := .betaRev f #[i]
2097+
let rbody ← core zα pα body
2098+
let pbody ← rbody.toNonneg
2099+
let pr : Q(∀ x, 0 ≤ $f x) ← mkLambdaFVars #[i] pbody
2100+
assertInstancesCommute
2101+
return .nonnegative q(integral_nonneg $pr)
2102+
| _ => throwError "not MeasureTheory.integral"
2103+
2104+
end Mathlib.Meta.Positivity

‎Mathlib/MeasureTheory/Measure/Tilted.lean‎

Lines changed: 8 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -90,8 +90,7 @@ lemma tilted_congr {g : α → ℝ} (hfg : f =ᵐ[μ] g) :
9090

9191
lemma tilted_eq_withDensity_nnreal (μ : Measure α) (f : α → ℝ) :
9292
μ.tilted f = μ.withDensity (fun x ↦ ((↑) : ℝ≥0 → ℝ≥0∞)
93-
(⟨exp (f x) / ∫ x, exp (f x) ∂μ,
94-
div_nonneg (exp_pos _).le (integral_nonneg (fun _ ↦ (exp_pos _).le))⟩ : ℝ≥0)) := by
93+
(⟨exp (f x) / ∫ x, exp (f x) ∂μ, by positivity⟩ : ℝ≥0)) := by
9594
rw [Measure.tilted]
9695
congr with x
9796
rw [ENNReal.ofReal_eq_coe_nnreal]
@@ -109,8 +108,7 @@ lemma tilted_apply_eq_ofReal_integral' {s : Set α} (f : α → ℝ) (hs : Measu
109108
by_cases hf : Integrable (fun x ↦ exp (f x)) μ
110109
· rw [tilted_apply' _ _ hs, ← ofReal_integral_eq_lintegral_ofReal]
111110
· exact hf.integrableOn.div_const _
112-
· exact ae_of_all _
113-
(fun _ ↦ div_nonneg (exp_pos _).le (integral_nonneg (fun _ ↦ (exp_pos _).le)))
111+
· exact ae_of_all _ (fun _ ↦ by positivity)
114112
· simp only [hf, not_false_eq_true, tilted_of_not_integrable, Measure.zero_toOuterMeasure,
115113
OuterMeasure.coe_zero, Pi.zero_apply, integral_undef hf, div_zero, integral_zero,
116114
ENNReal.ofReal_zero]
@@ -120,8 +118,7 @@ lemma tilted_apply_eq_ofReal_integral [SFinite μ] (f : α → ℝ) (s : Set α)
120118
by_cases hf : Integrable (fun x ↦ exp (f x)) μ
121119
· rw [tilted_apply _ _, ← ofReal_integral_eq_lintegral_ofReal]
122120
· exact hf.integrableOn.div_const _
123-
· exact ae_of_all _
124-
(fun _ ↦ div_nonneg (exp_pos _).le (integral_nonneg (fun _ ↦ (exp_pos _).le)))
121+
· exact ae_of_all _ (fun _ ↦ by positivity)
125122
· simp only [hf, not_false_eq_true, tilted_of_not_integrable, Measure.zero_toOuterMeasure,
126123
OuterMeasure.coe_zero, Pi.zero_apply, integral_undef hf, div_zero, integral_zero,
127124
ENNReal.ofReal_zero]
@@ -257,7 +254,7 @@ lemma tilted_tilted (hf : Integrable (fun x ↦ exp (f x)) μ) (g : α → ℝ)
257254
ext1 s hs
258255
rw [tilted_apply' _ _ hs, tilted_apply' _ _ hs, set_lintegral_tilted' f _ hs]
259256
congr with x
260-
rw [← ENNReal.ofReal_mul (div_nonneg (exp_pos _).le (integral_nonneg (fun _ ↦ (exp_pos _).le))),
257+
rw [← ENNReal.ofReal_mul (by positivity),
261258
integral_exp_tilted f, Pi.add_apply, exp_add]
262259
congr 1
263260
simp only [Pi.add_apply]
@@ -321,7 +318,7 @@ lemma toReal_rnDeriv_tilted_right (μ ν : Measure α) [SigmaFinite μ] [SigmaFi
321318
filter_upwards [rnDeriv_tilted_right μ ν hf] with x hx
322319
rw [hx]
323320
simp only [ENNReal.toReal_mul, gt_iff_lt, mul_eq_mul_right_iff, ENNReal.toReal_ofReal_eq_iff]
324-
exact Or.inl (mul_nonneg (exp_pos _).le (integral_nonneg (fun _ ↦ (exp_pos _).le)))
321+
exact Or.inl (by positivity)
325322

326323
lemma rnDeriv_tilted_left {ν : Measure α} [SigmaFinite μ] [SigmaFinite ν]
327324
(hfμ : AEMeasurable f μ) (hfν : AEMeasurable f ν) :
@@ -340,9 +337,7 @@ lemma toReal_rnDeriv_tilted_left {ν : Measure α} [SigmaFinite μ] [SigmaFinite
340337
filter_upwards [rnDeriv_tilted_left hfμ hfν] with x hx
341338
rw [hx]
342339
simp only [ENNReal.toReal_mul, mul_eq_mul_right_iff, ENNReal.toReal_ofReal_eq_iff]
343-
refine Or.inl (mul_nonneg (exp_pos _).le ?_)
344-
rw [inv_nonneg]
345-
exact (integral_nonneg (fun _ ↦ (exp_pos _).le))
340+
exact Or.inl (by positivity)
346341

347342
lemma rnDeriv_tilted_left_self [SigmaFinite μ] (hf : AEMeasurable f μ) :
348343
(μ.tilted f).rnDeriv μ =ᵐ[μ] fun x ↦ ENNReal.ofReal (exp (f x) / ∫ x, exp (f x) ∂μ) := by
@@ -358,8 +353,7 @@ lemma log_rnDeriv_tilted_left_self [SigmaFinite μ] (hf : Integrable (fun x ↦
358353
| inr h0 =>
359354
have hf' : AEMeasurable f μ := aemeasurable_of_aemeasurable_exp hf.1.aemeasurable
360355
filter_upwards [rnDeriv_tilted_left_self hf'] with x hx
361-
rw [hx, ENNReal.toReal_ofReal, log_div (exp_pos _).ne', log_exp]
362-
· exact (integral_exp_pos hf).ne'
363-
· exact div_nonneg (exp_pos _).le (integral_nonneg (fun _ ↦ (exp_pos _).le))
356+
rw [hx, ENNReal.toReal_ofReal (by positivity), log_div (exp_pos _).ne', log_exp]
357+
exact (integral_exp_pos hf).ne'
364358

365359
end MeasureTheory

‎Mathlib/Probability/Martingale/Upcrossing.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -741,7 +741,7 @@ theorem Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part [IsFin
741741
by_cases hab : a < b
742742
· exact mul_integral_upcrossingsBefore_le_integral_pos_part_aux hf hab
743743
· rw [not_lt, ← sub_nonpos] at hab
744-
exact le_trans (mul_nonpos_of_nonpos_of_nonneg hab (integral_nonneg fun ω => Nat.cast_nonneg _))
744+
exact le_trans (mul_nonpos_of_nonpos_of_nonneg hab (by positivity))
745745
(integral_nonneg fun ω => posPart_nonneg _)
746746
#align measure_theory.submartingale.mul_integral_upcrossings_before_le_integral_pos_part MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part
747747

0 commit comments

Comments
 (0)