theorem measurable_limUnder_of_exists_tendsto {ι : Type u_1} {X : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} [TopologicalSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [MeasurableSpace E] [BorelSpace E] {l : Filter ι} [l.IsCountablyGenerated] {f : ι → X → E} [hE : Nonempty E] (h_conv : ∀ (x : X), ∃ (c : E), Filter.Tendsto (fun (x_1 : ι) => f x_1 x) l (nhds c)) (hf : ∀ (i : ι), Measurable (f i)) : Measurable fun (x : X) => l.limUnder fun (x_1 : ι) => f x_1 x

theorem measurable_limUnder {ι : Type u_1} {X : Type u_2} {E : Type u_3} [MeasurableSpace X] [TopologicalSpace E] [PolishSpace E] [MeasurableSpace E] [BorelSpace E] [Countable ι] {l : Filter ι} [l.IsCountablyGenerated] {f : ι → X → E} [hE : Nonempty E] (hf : ∀ (i : ι), Measurable (f i)) : Measurable fun (x : X) => l.limUnder fun (x_1 : ι) => f x_1 x

theorem limUnder_prod {α : Type u_1} {β : Type u_2} {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [Nonempty X] [Nonempty Y] [T2Space X] [T2Space Y] {f : Filter α} {f' : Filter β} [f.NeBot] [f'.NeBot] {g : α → X} {g' : β → Y} (h₁ : ∃ (x : X), Filter.Tendsto g f (nhds x)) (h₂ : ∃ (x' : Y), Filter.Tendsto g' f' (nhds x')) : ((f ×ˢ f').limUnder fun (x : α × β) => (g x.1, g' x.2)) = (f.limUnder g, f'.limUnder g')

theorem Measurable.of_edist_eq_zero {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] [MeasurableSpace E] [BorelSpace E] {X Y : Ω → E} (hX : Measurable X) (h_eq_zero : ∀ (ω : Ω), EDist.edist (Y ω) (X ω) = 0) : Measurable Y

theorem edist_limUnder_const {T : Type u_1} {E : Type u_2} [PseudoEMetricSpace E] [Nonempty E] {c : E} {l : Filter T} [l.NeBot] : edist (l.limUnder fun (x : T) => c) c = 0

theorem edist_limUnder_prod_eq_zero {α : Type u_1} {β : Type u_2} {E : Type u_3} [PseudoEMetricSpace E] [Nonempty E] {l₁ : Filter α} {l₂ : Filter β} [l₁.NeBot] [l₂.NeBot] {f : α → E} {g : β → E} (hf : ∃ (c : E), Filter.Tendsto f l₁ (nhds c)) (hg : ∃ (c : E), Filter.Tendsto g l₂ (nhds c)) : edist ((l₁ ×ˢ l₂).limUnder fun (p : α × β) => (f p.1, g p.2)) (l₁.limUnder f, l₂.limUnder g) = 0

noncomputable def ProbabilityTheory.indicatorProcess {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [hE : Nonempty E] (X : T → Ω → E) (A : Set Ω) : T → Ω → E

Process where we replace the values for ω outside of A with a constant value.

Equations

• ProbabilityTheory.indicatorProcess X A t ω = if ω ∈ A then X t ω else hE.some

@[simp]

theorem ProbabilityTheory.indicatorProcess_apply {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [hE : Nonempty E] (X : T → Ω → E) (A : Set Ω) (t : T) (ω : Ω) [Decidable (ω ∈ A)] : indicatorProcess X A t ω = if ω ∈ A then X t ω else hE.some

theorem ProbabilityTheory.measurable_indicatorProcess {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {X : T → Ω → E} [hE : Nonempty E] [MeasurableSpace E] {A : Set Ω} (hA : MeasurableSet A) (hX : ∀ (t : T), Measurable (X t)) (t : T) : Measurable (indicatorProcess X A t)

theorem ProbabilityTheory.measurable_pair_indicatorProcess {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [hE : Nonempty E] {T₁ : Type u_4} {T₂ : Type u_5} [TopologicalSpace E] [MeasurableSpace E] [BorelSpace E] {X₁ : T₁ → Ω → E} {X₂ : T₂ → Ω → E} (hX₁ : ∀ (t : T₁), Measurable (X₁ t)) (hX₂ : ∀ (t : T₂), Measurable (X₂ t)) (hX₁₂ : ∀ (i : T₁) (j : T₂), Measurable fun (ω : Ω) => (X₁ i ω, X₂ j ω)) {A₁ A₂ : Set Ω} (hA₁ : MeasurableSet A₁) (hA₂ : MeasurableSet A₂) (s : T₁) (t : T₂) : Measurable fun (ω : Ω) => (indicatorProcess X₁ A₁ s ω, indicatorProcess X₂ A₂ t ω)

theorem ProbabilityTheory.measurable_edist_indicatorProcess {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [hE : Nonempty E] {T₁ : Type u_4} {T₂ : Type u_5} [PseudoEMetricSpace E] [MeasurableSpace E] [BorelSpace E] {X₁ : T₁ → Ω → E} {X₂ : T₂ → Ω → E} (hX₁ : ∀ (t : T₁), Measurable (X₁ t)) (hX₂ : ∀ (t : T₂), Measurable (X₂ t)) (hX₁₂ : ∀ (i : T₁) (j : T₂), Measurable fun (ω : Ω) => (X₁ i ω, X₂ j ω)) {A₁ A₂ : Set Ω} (hA₁ : MeasurableSet A₁) (hA₂ : MeasurableSet A₂) (s : T₁) (t : T₂) : Measurable fun (ω : Ω) => edist (indicatorProcess X₁ A₁ s ω) (indicatorProcess X₂ A₂ t ω)

def ProbabilityTheory.IsLimitOfIndicator {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] [hE : Nonempty E] [TopologicalSpace T] [SecondCountableTopology T] (Y X : T → Ω → E) (P : MeasureTheory.Measure Ω) (U : Set T) : Prop

A class of processes built from an other. Used to ensure measurability.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.IsLimitOfIndicator.measurable {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {U : Set T} [PseudoEMetricSpace E] [hE : Nonempty E] [TopologicalSpace T] [SecondCountableTopology T] [MeasurableSpace E] [BorelSpace E] {Y X : T → Ω → E} (hX : ∀ (t : T), Measurable (X t)) (hY : IsLimitOfIndicator Y X P U) (t : T) : Measurable (Y t)

theorem ProbabilityTheory.measurable_pair_limUnder_comap {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] [hE : Nonempty E] {T : Type u_4} [PseudoEMetricSpace T] {X₁ X₂ : T → Ω → E} {T' : Set T} (hT'_dense : Dense T') (hX₁₂ : ∀ (i j : T), Measurable fun (ω : Ω) => (X₁ i ω, X₂ j ω)) (s t : T) (hX₁_tendsto : ∀ (ω : Ω), ∃ (x : E), Filter.Tendsto (fun (t' : ↑T') => X₁ (↑t') ω) (Filter.comap Subtype.val (nhds s)) (nhds x)) (hX₂_tendsto : ∀ (ω : Ω), ∃ (x : E), Filter.Tendsto (fun (t' : ↑T') => X₂ (↑t') ω) (Filter.comap Subtype.val (nhds t)) (nhds x)) : Measurable fun (ω : Ω) => ((Filter.comap Subtype.val (nhds s)).limUnder fun (t' : ↑T') => X₁ (↑t') ω, (Filter.comap Subtype.val (nhds t)).limUnder fun (t' : ↑T') => X₂ (↑t') ω)

theorem ProbabilityTheory.measurable_pair_limUnder_indicatorProcess {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [PseudoEMetricSpace E] [hE : Nonempty E] {T : Type u_4} [PseudoEMetricSpace T] [SecondCountableTopology T] [MeasurableSpace E] [BorelSpace E] {X X' : T → Ω → E} (hX : ∀ (t : T), Measurable (X t)) (hX' : ∀ (t : T), Measurable (X' t)) (hX_pair : ∀ (i j : T), Measurable fun (ω : Ω) => (X i ω, X' j ω)) {A₁ A₂ : Set Ω} (hA₁ : MeasurableSet A₁) (hA₂ : MeasurableSet A₂) (s t : T) (h_tendsto₁ : ∀ ω ∈ A₁, ∃ (c : E), Filter.Tendsto (fun (t' : ↑(denseCountable T)) => X (↑t') ω) (Filter.comap Subtype.val (nhds s)) (nhds c)) (h_tendsto₂ : ∀ ω ∈ A₂, ∃ (c : E), Filter.Tendsto (fun (t' : ↑(denseCountable T)) => X' (↑t') ω) (Filter.comap Subtype.val (nhds t)) (nhds c)) : Measurable fun (ω : Ω) => ((Filter.comap Subtype.val (nhds s)).limUnder fun (t' : ↑(denseCountable T)) => indicatorProcess X A₁ (↑t') ω, (Filter.comap Subtype.val (nhds t)).limUnder fun (t' : ↑(denseCountable T)) => indicatorProcess X' A₂ (↑t') ω)

theorem ProbabilityTheory.IsLimitOfIndicator.measurable_pair {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [PseudoEMetricSpace E] [hE : Nonempty E] {T : Type u_4} [PseudoEMetricSpace T] [SecondCountableTopology T] [MeasurableSpace E] [BorelSpace E] {Y X Z X' : T → Ω → E} {U₁ U₂ : Set T} (hX : ∀ (t : T), Measurable (X t)) (hX' : ∀ (t : T), Measurable (X' t)) (hX_pair : ∀ (i j : T), Measurable fun (ω : Ω) => (X i ω, X' j ω)) (hY : IsLimitOfIndicator Y X P U₁) (hZ : IsLimitOfIndicator Z X' P U₂) (s t : T) : Measurable fun (ω : Ω) => (Y s ω, Z t ω)

theorem ProbabilityTheory.IsLimitOfIndicator.measurable_edist {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [PseudoEMetricSpace E] [hE : Nonempty E] {T : Type u_4} [PseudoEMetricSpace T] [SecondCountableTopology T] [MeasurableSpace E] [BorelSpace E] {Y X Z X' : T → Ω → E} {U₁ U₂ : Set T} (hX : ∀ (t : T), Measurable (X t)) (hX' : ∀ (t : T), Measurable (X' t)) (hX_pair : ∀ (i j : T), Measurable fun (ω : Ω) => (X i ω, X' j ω)) (hY : IsLimitOfIndicator Y X P U₁) (hZ : IsLimitOfIndicator Z X' P U₂) (s t : T) : Measurable fun (ω : Ω) => edist (Y s ω) (Z t ω)

theorem ProbabilityTheory.IsLimitOfIndicator.indicatorProcess {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {U : Set T} [PseudoEMetricSpace E] [hE : Nonempty E] [TopologicalSpace T] [SecondCountableTopology T] {Y X : T → Ω → E} (hY : IsLimitOfIndicator Y X P U) (A : Set Ω) (hA_meas : MeasurableSet A) (hA_ae : ∀ᵐ (ω : Ω) ∂P, ω ∈ A) : IsLimitOfIndicator (fun (t : T) => ProbabilityTheory.indicatorProcess Y A t) X P U