diff --git a/Mathlib/Probability/IdentDistrib.lean b/Mathlib/Probability/IdentDistrib.lean index 0e7cb86dfd7ed5..6ee6ef0b727d39 100644 --- a/Mathlib/Probability/IdentDistrib.lean +++ b/Mathlib/Probability/IdentDistrib.lean @@ -140,12 +140,13 @@ theorem ae_mem_snd (h : IdentDistrib f g μ ν) {t : Set γ} (tmeas : Measurable /-- In a second countable topology, the first function in an identically distributed pair is a.e. strongly measurable. So is the second function, but use `h.symm.aestronglyMeasurable_fst` as `h.aestronglyMeasurable_snd` has a different meaning. -/ -theorem aestronglyMeasurable_fst [TopologicalSpace γ] [MetrizableSpace γ] [OpensMeasurableSpace γ] - [SecondCountableTopology γ] (h : IdentDistrib f g μ ν) : AEStronglyMeasurable f μ := +theorem aestronglyMeasurable_fst [TopologicalSpace γ] [PseudoMetrizableSpace γ] + [OpensMeasurableSpace γ] [SecondCountableTopology γ] (h : IdentDistrib f g μ ν) : + AEStronglyMeasurable f μ := h.aemeasurable_fst.aestronglyMeasurable /-- If `f` and `g` are identically distributed and `f` is a.e. strongly measurable, so is `g`. -/ -theorem aestronglyMeasurable_snd [TopologicalSpace γ] [MetrizableSpace γ] [BorelSpace γ] +theorem aestronglyMeasurable_snd [TopologicalSpace γ] [PseudoMetrizableSpace γ] [BorelSpace γ] (h : IdentDistrib f g μ ν) (hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable g ν := by refine aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨h.aemeasurable_snd, ?_⟩ rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 hf).2 with ⟨t, t_sep, ht⟩ @@ -153,7 +154,7 @@ theorem aestronglyMeasurable_snd [TopologicalSpace γ] [MetrizableSpace γ] [Bor apply h.ae_mem_snd isClosed_closure.measurableSet filter_upwards [ht] with x hx using subset_closure hx -theorem aestronglyMeasurable_iff [TopologicalSpace γ] [MetrizableSpace γ] [BorelSpace γ] +theorem aestronglyMeasurable_iff [TopologicalSpace γ] [PseudoMetrizableSpace γ] [BorelSpace γ] (h : IdentDistrib f g μ ν) : AEStronglyMeasurable f μ ↔ AEStronglyMeasurable g ν := ⟨fun hf => h.aestronglyMeasurable_snd hf, fun hg => h.symm.aestronglyMeasurable_snd hg⟩ @@ -227,11 +228,12 @@ theorem integrable_iff [NormedAddCommGroup γ] [BorelSpace γ] (h : IdentDistrib Integrable f μ ↔ Integrable g ν := ⟨fun hf => h.integrable_snd hf, fun hg => h.symm.integrable_snd hg⟩ -protected theorem norm [NormedAddCommGroup γ] [BorelSpace γ] (h : IdentDistrib f g μ ν) : +protected theorem norm [NormedAddCommGroup γ] [OpensMeasurableSpace γ] (h : IdentDistrib f g μ ν) : IdentDistrib (fun x => ‖f x‖) (fun x => ‖g x‖) μ ν := h.comp measurable_norm -protected theorem nnnorm [NormedAddCommGroup γ] [BorelSpace γ] (h : IdentDistrib f g μ ν) : +protected theorem nnnorm [NormedAddCommGroup γ] [OpensMeasurableSpace γ] + (h : IdentDistrib f g μ ν) : IdentDistrib (fun x => ‖f x‖₊) (fun x => ‖g x‖₊) μ ν := h.comp measurable_nnnorm diff --git a/Mathlib/Probability/Independence/Integrable.lean b/Mathlib/Probability/Independence/Integrable.lean index 415bb0fd90a1bc..129795615509e4 100644 --- a/Mathlib/Probability/Independence/Integrable.lean +++ b/Mathlib/Probability/Independence/Integrable.lean @@ -21,7 +21,7 @@ open scoped ENNReal NNReal Topology namespace MeasureTheory variable {Ω E F : Type*} [MeasurableSpace Ω] {μ : Measure Ω} - [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] + [NormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] [MeasurableSpace F] /-- If a nonzero function belongs to `ℒ^p` and is independent of another function, then diff --git a/Mathlib/Probability/Integration.lean b/Mathlib/Probability/Integration.lean index 5a3d3108ae1ff7..e0f6c3798d5dae 100644 --- a/Mathlib/Probability/Integration.lean +++ b/Mathlib/Probability/Integration.lean @@ -160,7 +160,8 @@ theorem IndepFun.integrable_mul {β : Type*} [MeasurableSpace β] {X Y : Ω → /-- If the product of two independent real-valued random variables is integrable and the second one is not almost everywhere zero, then the first one is integrable. -/ theorem IndepFun.integrable_left_of_integrable_mul {β : Type*} [MeasurableSpace β] {X Y : Ω → β} - [NormedDivisionRing β] [BorelSpace β] (hXY : IndepFun X Y μ) (h'XY : Integrable (X * Y) μ) + [NormedDivisionRing β] [OpensMeasurableSpace β] + (hXY : IndepFun X Y μ) (h'XY : Integrable (X * Y) μ) (hX : AEStronglyMeasurable X μ) (hY : AEStronglyMeasurable Y μ) (h'Y : ¬Y =ᵐ[μ] 0) : Integrable X μ := by refine ⟨hX, ?_⟩ @@ -179,7 +180,8 @@ theorem IndepFun.integrable_left_of_integrable_mul {β : Type*} [MeasurableSpace /-- If the product of two independent real-valued random variables is integrable and the first one is not almost everywhere zero, then the second one is integrable. -/ theorem IndepFun.integrable_right_of_integrable_mul {β : Type*} [MeasurableSpace β] {X Y : Ω → β} - [NormedDivisionRing β] [BorelSpace β] (hXY : IndepFun X Y μ) (h'XY : Integrable (X * Y) μ) + [NormedDivisionRing β] [OpensMeasurableSpace β] + (hXY : IndepFun X Y μ) (h'XY : Integrable (X * Y) μ) (hX : AEStronglyMeasurable X μ) (hY : AEStronglyMeasurable Y μ) (h'X : ¬X =ᵐ[μ] 0) : Integrable Y μ := by refine ⟨hY, ?_⟩ diff --git a/Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean b/Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean index 96e39a42d746ee..468172073f8b69 100644 --- a/Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean +++ b/Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean @@ -190,11 +190,11 @@ lemma dirac_unit_compProd (κ : Kernel Unit β) [IsSFiniteKernel κ] : Measure.dirac () ⊗ₘ κ = (κ ()).map (Prod.mk ()) := by ext s hs; rw [dirac_compProd_apply hs, Measure.map_apply measurable_prodMk_left hs] -lemma dirac_unit_compProd_const (μ : Measure β) [IsFiniteMeasure μ] : +lemma dirac_unit_compProd_const (μ : Measure β) [SFinite μ] : Measure.dirac () ⊗ₘ Kernel.const Unit μ = μ.map (Prod.mk ()) := by rw [dirac_unit_compProd, Kernel.const_apply] -lemma snd_dirac_unit_compProd_const (μ : Measure β) [IsFiniteMeasure μ] : +lemma snd_dirac_unit_compProd_const (μ : Measure β) [SFinite μ] : snd (Measure.dirac () ⊗ₘ Kernel.const Unit μ) = μ := by simp instance : SFinite (μ ⊗ₘ κ) := by rw [compProd]; infer_instance @@ -275,7 +275,7 @@ lemma absolutelyContinuous_of_compProd [SFinite μ] [IsSFiniteKernel κ] [h_zero exact (h_zero a).out lemma absolutelyContinuous_compProd_left_iff [SFinite μ] [SFinite ν] - [IsFiniteKernel κ] [∀ a, NeZero (κ a)] : + [IsSFiniteKernel κ] [∀ a, NeZero (κ a)] : μ ⊗ₘ κ ≪ ν ⊗ₘ κ ↔ μ ≪ ν := ⟨absolutelyContinuous_of_compProd, fun h ↦ h.compProd_left κ⟩ diff --git a/Mathlib/Probability/Kernel/RadonNikodym.lean b/Mathlib/Probability/Kernel/RadonNikodym.lean index b1612fefe732df..033dd3e211b27e 100644 --- a/Mathlib/Probability/Kernel/RadonNikodym.lean +++ b/Mathlib/Probability/Kernel/RadonNikodym.lean @@ -292,7 +292,7 @@ lemma singularPart_compl_mutuallySingularSetSlice (κ η : Kernel α γ) [IsSFin · simp only [sub_nonneg, hx.le] · simp only [sub_pos, hx] -lemma singularPart_of_subset_compl_mutuallySingularSetSlice [IsFiniteKernel κ] +lemma singularPart_of_subset_compl_mutuallySingularSetSlice [IsSFiniteKernel κ] [IsFiniteKernel η] {a : α} {s : Set γ} (hs : s ⊆ (mutuallySingularSetSlice κ η a)ᶜ) : singularPart κ η a s = 0 := measure_mono_null hs (singularPart_compl_mutuallySingularSetSlice κ η a) @@ -392,8 +392,8 @@ lemma rnDeriv_add_singularPart (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFin section EqZeroIff -lemma singularPart_eq_zero_iff_apply_eq_zero (κ η : Kernel α γ) [IsFiniteKernel κ] - [IsFiniteKernel η] (a : α) : +lemma singularPart_eq_zero_iff_apply_eq_zero (κ η : Kernel α γ) [IsSFiniteKernel κ] + [IsSFiniteKernel η] (a : α) : singularPart κ η a = 0 ↔ singularPart κ η a (mutuallySingularSetSlice κ η a) = 0 := by rw [← Measure.measure_univ_eq_zero] have : univ = (mutuallySingularSetSlice κ η a) ∪ (mutuallySingularSetSlice κ η a)ᶜ := by simp diff --git a/Mathlib/Probability/Martingale/Basic.lean b/Mathlib/Probability/Martingale/Basic.lean index f0e94f01ce80c9..d42606bc309a81 100644 --- a/Mathlib/Probability/Martingale/Basic.lean +++ b/Mathlib/Probability/Martingale/Basic.lean @@ -66,7 +66,8 @@ theorem martingale_const (ℱ : Filtration ι m0) (μ : Measure Ω) [IsFiniteMea Martingale (fun _ _ => x) ℱ μ := ⟨adapted_const ℱ _, fun i j _ => by rw [condExp_const (ℱ.le _)]⟩ -theorem martingale_const_fun [OrderBot ι] (ℱ : Filtration ι m0) (μ : Measure Ω) [IsFiniteMeasure μ] +theorem martingale_const_fun [OrderBot ι] (ℱ : Filtration ι m0) (μ : Measure Ω) + [SigmaFiniteFiltration μ ℱ] {f : Ω → E} (hf : StronglyMeasurable[ℱ ⊥] f) (hfint : Integrable f μ) : Martingale (fun _ => f) ℱ μ := by refine ⟨fun i => hf.mono <| ℱ.mono bot_le, fun i j _ => ?_⟩ @@ -250,7 +251,8 @@ end Submartingale section Submartingale -theorem submartingale_of_setIntegral_le [IsFiniteMeasure μ] {f : ι → Ω → ℝ} (hadp : Adapted ℱ f) +theorem submartingale_of_setIntegral_le [SigmaFiniteFiltration μ ℱ] + {f : ι → Ω → ℝ} (hadp : Adapted ℱ f) (hint : ∀ i, Integrable (f i) μ) (hf : ∀ i j : ι, i ≤ j → ∀ s : Set Ω, MeasurableSet[ℱ i] s → ∫ ω in s, f i ω ∂μ ≤ ∫ ω in s, f j ω ∂μ) : Submartingale f ℱ μ := by @@ -267,7 +269,8 @@ theorem submartingale_of_setIntegral_le [IsFiniteMeasure μ] {f : ι → Ω → integral_sub' integrable_condExp.integrableOn (hint i).integrableOn, sub_nonneg, setIntegral_condExp (ℱ.le i) (hint j) hs] -theorem submartingale_of_condExp_sub_nonneg [IsFiniteMeasure μ] {f : ι → Ω → ℝ} (hadp : Adapted ℱ f) +theorem submartingale_of_condExp_sub_nonneg [SigmaFiniteFiltration μ ℱ] + {f : ι → Ω → ℝ} (hadp : Adapted ℱ f) (hint : ∀ i, Integrable (f i) μ) (hf : ∀ i j, i ≤ j → 0 ≤ᵐ[μ] μ[f j - f i|ℱ i]) : Submartingale f ℱ μ := by refine ⟨hadp, fun i j hij => ?_, hint⟩ @@ -289,7 +292,7 @@ theorem Submartingale.condExp_sub_nonneg {f : ι → Ω → ℝ} (hf : Submartin @[deprecated (since := "2025-01-21")] alias Submartingale.condexp_sub_nonneg := Submartingale.condExp_sub_nonneg -theorem submartingale_iff_condExp_sub_nonneg [IsFiniteMeasure μ] {f : ι → Ω → ℝ} : +theorem submartingale_iff_condExp_sub_nonneg [SigmaFiniteFiltration μ ℱ] {f : ι → Ω → ℝ} : Submartingale f ℱ μ ↔ Adapted ℱ f ∧ (∀ i, Integrable (f i) μ) ∧ ∀ i j, i ≤ j → 0 ≤ᵐ[μ] μ[f j - f i|ℱ i] := ⟨fun h => ⟨h.adapted, h.integrable, fun _ _ => h.condExp_sub_nonneg⟩, fun ⟨hadp, hint, h⟩ => diff --git a/Mathlib/Probability/Process/Adapted.lean b/Mathlib/Probability/Process/Adapted.lean index 42164e6123f0fc..e785972307b22b 100644 --- a/Mathlib/Probability/Process/Adapted.lean +++ b/Mathlib/Probability/Process/Adapted.lean @@ -58,10 +58,10 @@ protected theorem div [Div β] [ContinuousDiv β] (hu : Adapted f u) (hv : Adapt Adapted f (u / v) := fun i => (hu i).div (hv i) @[to_additive] -protected theorem inv [Group β] [IsTopologicalGroup β] (hu : Adapted f u) : +protected theorem inv [Group β] [ContinuousInv β] (hu : Adapted f u) : Adapted f u⁻¹ := fun i => (hu i).inv -protected theorem smul [SMul ℝ β] [ContinuousSMul ℝ β] (c : ℝ) (hu : Adapted f u) : +protected theorem smul [SMul ℝ β] [ContinuousConstSMul ℝ β] (c : ℝ) (hu : Adapted f u) : Adapted f (c • u) := fun i => (hu i).const_smul c protected theorem stronglyMeasurable {i : ι} (hf : Adapted f u) : StronglyMeasurable[m] (u i) := @@ -111,7 +111,7 @@ protected theorem adapted (h : ProgMeasurable f u) : Adapted f u := by rw [this] exact (h i).comp_measurable measurable_prodMk_left -protected theorem comp {t : ι → Ω → ι} [TopologicalSpace ι] [BorelSpace ι] [MetrizableSpace ι] +protected theorem comp {t : ι → Ω → ι} [TopologicalSpace ι] [BorelSpace ι] [PseudoMetrizableSpace ι] (h : ProgMeasurable f u) (ht : ProgMeasurable f t) (ht_le : ∀ i ω, t i ω ≤ i) : ProgMeasurable f fun i ω => u (t i ω) ω := by intro i @@ -141,11 +141,11 @@ protected theorem finset_prod {γ} [CommMonoid β] [ContinuousMul β] {U : γ convert ProgMeasurable.finset_prod' h using 1; ext (i a); simp only [Finset.prod_apply] @[to_additive] -protected theorem inv [Group β] [IsTopologicalGroup β] (hu : ProgMeasurable f u) : +protected theorem inv [Group β] [ContinuousInv β] (hu : ProgMeasurable f u) : ProgMeasurable f fun i ω => (u i ω)⁻¹ := fun i => (hu i).inv @[to_additive] -protected theorem div [Group β] [IsTopologicalGroup β] (hu : ProgMeasurable f u) +protected theorem div [Group β] [ContinuousDiv β] (hu : ProgMeasurable f u) (hv : ProgMeasurable f v) : ProgMeasurable f fun i ω => u i ω / v i ω := fun i => (hu i).div (hv i) diff --git a/Mathlib/Probability/Process/Stopping.lean b/Mathlib/Probability/Process/Stopping.lean index f9fe64ed231109..2ffc6207518a64 100644 --- a/Mathlib/Probability/Process/Stopping.lean +++ b/Mathlib/Probability/Process/Stopping.lean @@ -719,7 +719,7 @@ section ProgMeasurable variable [MeasurableSpace ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [BorelSpace ι] [TopologicalSpace β] {u : ι → Ω → β} {τ : Ω → ι} {f : Filtration ι m} -theorem progMeasurable_min_stopping_time [MetrizableSpace ι] (hτ : IsStoppingTime f τ) : +theorem progMeasurable_min_stopping_time [PseudoMetrizableSpace ι] (hτ : IsStoppingTime f τ) : ProgMeasurable f fun i ω => min i (τ ω) := by intro i let m_prod : MeasurableSpace (Set.Iic i × Ω) := Subtype.instMeasurableSpace.prod (f i) @@ -756,15 +756,15 @@ theorem progMeasurable_min_stopping_time [MetrizableSpace ι] (hτ : IsStoppingT convert ω.prop simp only [sc, s, not_le, Set.mem_compl_iff, Set.mem_setOf_eq] -theorem ProgMeasurable.stoppedProcess [MetrizableSpace ι] (h : ProgMeasurable f u) +theorem ProgMeasurable.stoppedProcess [PseudoMetrizableSpace ι] (h : ProgMeasurable f u) (hτ : IsStoppingTime f τ) : ProgMeasurable f (stoppedProcess u τ) := h.comp (progMeasurable_min_stopping_time hτ) fun _ _ => min_le_left _ _ -theorem ProgMeasurable.adapted_stoppedProcess [MetrizableSpace ι] (h : ProgMeasurable f u) +theorem ProgMeasurable.adapted_stoppedProcess [PseudoMetrizableSpace ι] (h : ProgMeasurable f u) (hτ : IsStoppingTime f τ) : Adapted f (MeasureTheory.stoppedProcess u τ) := (h.stoppedProcess hτ).adapted -theorem ProgMeasurable.stronglyMeasurable_stoppedProcess [MetrizableSpace ι] +theorem ProgMeasurable.stronglyMeasurable_stoppedProcess [PseudoMetrizableSpace ι] (hu : ProgMeasurable f u) (hτ : IsStoppingTime f τ) (i : ι) : StronglyMeasurable (MeasureTheory.stoppedProcess u τ i) := (hu.adapted_stoppedProcess hτ i).mono (f.le _) @@ -778,7 +778,7 @@ theorem stronglyMeasurable_stoppedValue_of_le (h : ProgMeasurable f u) (hτ : Is refine StronglyMeasurable.comp_measurable (h n) ?_ exact (hτ.measurable_of_le hτ_le).subtype_mk.prodMk measurable_id -theorem measurable_stoppedValue [MetrizableSpace β] [MeasurableSpace β] [BorelSpace β] +theorem measurable_stoppedValue [PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] (hf_prog : ProgMeasurable f u) (hτ : IsStoppingTime f τ) : Measurable[hτ.measurableSpace] (stoppedValue u τ) := by have h_str_meas : ∀ i, StronglyMeasurable[f i] (stoppedValue u fun ω => min (τ ω) i) := fun i =>