ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>f : β × Ω → F<VAR>hX : AEMeasurable X μ<VAR>hY : AEMeasurable Y μ<VAR>hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)<GOAL>∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (fun ω => f (X a, ω)) ((ProbabilityTheory.condDistrib Y X μ) (X a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>f : β × Ω → F<VAR>hY : AEMeasurable Y μ<VAR>hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)<GOAL>MeasureTheory.Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂(ProbabilityTheory.condDistrib Y X μ) x) (MeasureTheory.Measure.map X μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>f : β × Ω → F<VAR>hX : AEMeasurable X μ<VAR>hY : AEMeasurable Y μ<VAR>hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)<GOAL>MeasureTheory.Integrable (fun a => ∫ (y : Ω), ‖f (X a, y)‖ ∂(ProbabilityTheory.condDistrib Y X μ) (X a)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>f : β × Ω → F<VAR>NormedSpace ℝ F<VAR>hY : AEMeasurable Y μ<VAR>hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)<GOAL>MeasureTheory.Integrable (fun x => ‖∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x‖) (MeasureTheory.Measure.map X μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>f : β × Ω → F<VAR>NormedSpace ℝ F<VAR>hX : AEMeasurable X μ<VAR>hY : AEMeasurable Y μ<VAR>hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)<GOAL>MeasureTheory.Integrable (fun a => ‖∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)‖) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>f : β × Ω → F<VAR>NormedSpace ℝ F<VAR>hY : AEMeasurable Y μ<VAR>hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)<GOAL>MeasureTheory.Integrable (fun x => ∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x) (MeasureTheory.Measure.map X μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>f : β × Ω → F<VAR>NormedSpace ℝ F<VAR>hX : AEMeasurable X μ<VAR>hY : AEMeasurable Y μ<VAR>hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)<GOAL>MeasureTheory.Integrable (fun a => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>hX : Measurable X<VAR>hY : AEMeasurable Y μ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>∫⁻ (a : α) in X ⁻¹' t, ((ProbabilityTheory.condDistrib Y X μ) (X a)) s ∂μ = μ (X ⁻¹' t ∩ Y ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>hX : Measurable X<VAR>hY : AEMeasurable Y μ<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>∫⁻ (a : α) in t, ((ProbabilityTheory.condDistrib Y X μ) (X a)) s ∂μ = μ (t ∩ Y ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>hX : Measurable X<VAR>hY : Measurable Y<VAR>hs : MeasurableSet s<GOAL>(fun a => (((ProbabilityTheory.condDistrib Y X μ) (X a)) s).toReal) =ᵐ[μ] μ[(Y ⁻¹' s).indicator fun ω => 1|MeasurableSpace.comap X mβ]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>f : β × Ω → F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>hX : Measurable X<VAR>hY : AEMeasurable Y μ<VAR>hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)<GOAL>μ[fun a => f (X a, Y a)|MeasurableSpace.comap X mβ] =ᵐ[μ] fun a => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>f : β × Ω → F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>hX : Measurable X<VAR>hY : AEMeasurable Y μ<VAR>hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)<VAR>hf_int : MeasureTheory.Integrable (fun a => f (X a, Y a)) μ<GOAL>μ[fun a => f (X a, Y a)|MeasurableSpace.comap X mβ] =ᵐ[μ] fun a => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>f : β × Ω → F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>hX : Measurable X<VAR>hY : AEMeasurable Y μ<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hf_int : MeasureTheory.Integrable (fun a => f (X a, Y a)) μ<GOAL>μ[fun a => f (X a, Y a)|MeasurableSpace.comap X mβ] =ᵐ[μ] fun a => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>hX : Measurable X<VAR>hY : AEMeasurable Y μ<VAR>f : Ω → F<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hf_int : MeasureTheory.Integrable (fun a => f (Y a)) μ<GOAL>μ[fun a => f (Y a)|MeasurableSpace.comap X mβ] =ᵐ[μ] fun a => ∫ (y : Ω), f y ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>X : α → β<VAR>mβ : MeasurableSpace β<VAR>Ω : Type u_5<VAR>NormedAddCommGroup Ω<VAR>NormedSpace ℝ Ω<VAR>CompleteSpace Ω<VAR>MeasurableSpace Ω<VAR>BorelSpace Ω<VAR>SecondCountableTopology Ω<VAR>Y : α → Ω<VAR>hX : Measurable X<VAR>hY_int : MeasureTheory.Integrable Y μ<GOAL>μ[Y|MeasurableSpace.comap X mβ] =ᵐ[μ] fun a => ∫ (y : Ω), y ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
<VAR>β : Type u_2<VAR>mβ : MeasurableSpace β<VAR>Ω : Type u_5<VAR>F : Type u_6<VAR>mΩ : MeasurableSpace Ω<VAR>X : Ω → β<VAR>μ : MeasureTheory.Measure Ω<VAR>TopologicalSpace F<VAR>f : Ω → F<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => f x.2) (MeasureTheory.Measure.map (fun ω => (X ω, ω)) μ)
<VAR>β : Type u_2<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>mβ : MeasurableSpace β<VAR>Ω : Type u_5<VAR>mΩ : MeasurableSpace Ω<VAR>X : Ω → β<VAR>μ : MeasureTheory.Measure Ω<VAR>f : Ω → F<VAR>hf_int : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun x => f x.2) (MeasureTheory.Measure.map (fun ω => (X ω, ω)) μ)
<VAR>β : Type u_2<VAR>mβ : MeasurableSpace β<VAR>Ω : Type u_5<VAR>F : Type u_6<GOAL>∀ {x : MeasurableSpace Ω} [inst : TopologicalSpace F] {X : Ω → β} {μ : MeasureTheory.Measure Ω}, Measurable X → ∀ {f : Ω → F}, MeasureTheory.AEStronglyMeasurable (fun x => f x.2) (MeasureTheory.Measure.map (fun ω => (X ω, ω)) μ) ↔ MeasureTheory.AEStronglyMeasurable f μ
<VAR>β : Type u_2<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>mβ : MeasurableSpace β<VAR>Ω : Type u_5<GOAL>∀ {x : MeasurableSpace Ω} {X : Ω → β} {μ : MeasureTheory.Measure Ω}, Measurable X → ∀ {f : Ω → F}, MeasureTheory.Integrable (fun x => f x.2) (MeasureTheory.Measure.map (fun ω => (X ω, ω)) μ) ↔ MeasureTheory.Integrable f μ
<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>NormedAddCommGroup F<VAR>mβ : MeasurableSpace β<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>X : Ω → β<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hX : Measurable X<VAR>f : Ω → F<VAR>hf_int : MeasureTheory.Integrable f μ<GOAL>μ[f|MeasurableSpace.comap X mβ] =ᵐ[μ] fun a => ∫ (y : Ω), f y ∂(ProbabilityTheory.condDistrib id X μ) (X a)
<VAR>μ : MeasureTheory.Measure ℝ<VAR>x : ℝ<GOAL>0 ≤ ↑(ProbabilityTheory.cdf μ) x
<VAR>μ : MeasureTheory.Measure ℝ<VAR>x : ℝ<GOAL>↑(ProbabilityTheory.cdf μ) x ≤ 1
<VAR>μ : MeasureTheory.Measure ℝ<GOAL>Monotone ↑(ProbabilityTheory.cdf μ)
<VAR>μ : MeasureTheory.Measure ℝ<GOAL>Filter.Tendsto (↑(ProbabilityTheory.cdf μ)) Filter.atBot (𝓝 0)
<VAR>μ : MeasureTheory.Measure ℝ<GOAL>Filter.Tendsto (↑(ProbabilityTheory.cdf μ)) Filter.atTop (𝓝 1)
<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>x : ℝ<GOAL>ENNReal.ofReal (↑(ProbabilityTheory.cdf μ) x) = μ (Set.Iic x)
<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>x : ℝ<GOAL>↑(ProbabilityTheory.cdf μ) x = (μ (Set.Iic x)).toReal
<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>(ProbabilityTheory.cdf μ).measure = μ
<VAR>f : StieltjesFunction<VAR>hf0 : Filter.Tendsto (↑f) Filter.atBot (𝓝 0)<VAR>hf1 : Filter.Tendsto (↑f) Filter.atTop (𝓝 1)<GOAL>ProbabilityTheory.cdf f.measure = f
<VAR>μ ν : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>MeasureTheory.IsProbabilityMeasure ν<VAR>h : ProbabilityTheory.cdf μ = ProbabilityTheory.cdf ν<GOAL>μ = ν
<VAR>μ ν : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>MeasureTheory.IsProbabilityMeasure ν<GOAL>ProbabilityTheory.cdf μ = ProbabilityTheory.cdf ν ↔ μ = ν
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u v : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>Mul β<VAR>ContinuousMul β<VAR>hu : MeasureTheory.Adapted f u<VAR>hv : MeasureTheory.Adapted f v<GOAL>MeasureTheory.Adapted f (u * v)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u v : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>Add β<VAR>ContinuousAdd β<VAR>hu : MeasureTheory.Adapted f u<VAR>hv : MeasureTheory.Adapted f v<GOAL>MeasureTheory.Adapted f (u + v)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u v : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>Div β<VAR>ContinuousDiv β<VAR>hu : MeasureTheory.Adapted f u<VAR>hv : MeasureTheory.Adapted f v<GOAL>MeasureTheory.Adapted f (u / v)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u v : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>Sub β<VAR>ContinuousSub β<VAR>hu : MeasureTheory.Adapted f u<VAR>hv : MeasureTheory.Adapted f v<GOAL>MeasureTheory.Adapted f (u - v)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>Group β<VAR>TopologicalGroup β<VAR>hu : MeasureTheory.Adapted f u<GOAL>MeasureTheory.Adapted f u⁻¹
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>hu : MeasureTheory.Adapted f u<GOAL>MeasureTheory.Adapted f (-u)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>SMul ℝ β<VAR>ContinuousSMul ℝ β<VAR>c : ℝ<VAR>hu : MeasureTheory.Adapted f u<GOAL>MeasureTheory.Adapted f (c • u)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>i : ι<VAR>hf : MeasureTheory.Adapted f u<GOAL>MeasureTheory.StronglyMeasurable (u i)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>i j : ι<VAR>hf : MeasureTheory.Adapted f u<VAR>hij : i ≤ j<GOAL>MeasureTheory.StronglyMeasurable (u i)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>x : β<GOAL>MeasureTheory.Adapted f fun x_1 x_2 => x
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>Zero β<VAR>f : MeasureTheory.Filtration ι m<GOAL>MeasureTheory.Adapted f 0
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>TopologicalSpace.MetrizableSpace β<VAR>mβ : MeasurableSpace β<VAR>BorelSpace β<VAR>u : ι → Ω → β<VAR>hum : ∀ (i : ι), MeasureTheory.StronglyMeasurable (u i)<GOAL>MeasureTheory.Adapted (MeasureTheory.Filtration.natural u hum) u
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>MeasurableSpace ι<VAR>f : MeasureTheory.Filtration ι m<VAR>b : β<GOAL>MeasureTheory.ProgMeasurable f fun x x => b
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>MeasurableSpace ι<VAR>h : MeasureTheory.ProgMeasurable f u<GOAL>MeasureTheory.Adapted f u
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>MeasurableSpace ι<VAR>t : ι → Ω → ι<VAR>TopologicalSpace ι<VAR>BorelSpace ι<VAR>TopologicalSpace.MetrizableSpace ι<VAR>h : MeasureTheory.ProgMeasurable f u<VAR>ht : MeasureTheory.ProgMeasurable f t<VAR>ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i<GOAL>MeasureTheory.ProgMeasurable f fun i ω => u (t i ω) ω
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u v : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>MeasurableSpace ι<VAR>Add β<VAR>ContinuousAdd β<VAR>hu : MeasureTheory.ProgMeasurable f u<VAR>hv : MeasureTheory.ProgMeasurable f v<GOAL>MeasureTheory.ProgMeasurable f fun i ω => u i ω + v i ω
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u v : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>MeasurableSpace ι<VAR>Mul β<VAR>ContinuousMul β<VAR>hu : MeasureTheory.ProgMeasurable f u<VAR>hv : MeasureTheory.ProgMeasurable f v<GOAL>MeasureTheory.ProgMeasurable f fun i ω => u i ω * v i ω
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>MeasurableSpace ι<VAR>γ : Type u_4<VAR>CommMonoid β<VAR>ContinuousMul β<VAR>U : γ → ι → Ω → β<VAR>s : Finset γ<VAR>h : ∀ c ∈ s, MeasureTheory.ProgMeasurable f (U c)<GOAL>MeasureTheory.ProgMeasurable f (∏ c ∈ s, U c)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>MeasurableSpace ι<VAR>γ : Type u_4<VAR>AddCommMonoid β<VAR>ContinuousAdd β<VAR>U : γ → ι → Ω → β<VAR>s : Finset γ<VAR>h : ∀ c ∈ s, MeasureTheory.ProgMeasurable f (U c)<GOAL>MeasureTheory.ProgMeasurable f (∑ c ∈ s, U c)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>MeasurableSpace ι<VAR>γ : Type u_4<VAR>CommMonoid β<VAR>ContinuousMul β<VAR>U : γ → ι → Ω → β<VAR>s : Finset γ<VAR>h : ∀ c ∈ s, MeasureTheory.ProgMeasurable f (U c)<GOAL>MeasureTheory.ProgMeasurable f fun i a => ∏ c ∈ s, U c i a
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>MeasurableSpace ι<VAR>γ : Type u_4<VAR>AddCommMonoid β<VAR>ContinuousAdd β<VAR>U : γ → ι → Ω → β<VAR>s : Finset γ<VAR>h : ∀ c ∈ s, MeasureTheory.ProgMeasurable f (U c)<GOAL>MeasureTheory.ProgMeasurable f fun i a => ∑ c ∈ s, U c i a
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>MeasurableSpace ι<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>hu : MeasureTheory.ProgMeasurable f u<GOAL>MeasureTheory.ProgMeasurable f fun i ω => -u i ω
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>MeasurableSpace ι<VAR>Group β<VAR>TopologicalGroup β<VAR>hu : MeasureTheory.ProgMeasurable f u<GOAL>MeasureTheory.ProgMeasurable f fun i ω => (u i ω)⁻¹
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u v : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>MeasurableSpace ι<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>hu : MeasureTheory.ProgMeasurable f u<VAR>hv : MeasureTheory.ProgMeasurable f v<GOAL>MeasureTheory.ProgMeasurable f fun i ω => u i ω - v i ω
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u v : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>MeasurableSpace ι<VAR>Group β<VAR>TopologicalGroup β<VAR>hu : MeasureTheory.ProgMeasurable f u<VAR>hv : MeasureTheory.ProgMeasurable f v<GOAL>MeasureTheory.ProgMeasurable f fun i ω => u i ω / v i ω
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>γ : Type u_4<VAR>MeasurableSpace ι<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>fltr : Filter γ<VAR>fltr.NeBot<VAR>fltr.IsCountablyGenerated<VAR>U : γ → ι → Ω → β<VAR>h : ∀ (l : γ), MeasureTheory.ProgMeasurable f (U l)<VAR>h_tendsto : Filter.Tendsto U fltr (𝓝 u)<GOAL>MeasureTheory.ProgMeasurable f u
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>MeasurableSpace ι<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>U : ℕ → ι → Ω → β<VAR>h : ∀ (l : ℕ), MeasureTheory.ProgMeasurable f (U l)<VAR>h_tendsto : Filter.Tendsto U Filter.atTop (𝓝 u)<GOAL>MeasureTheory.ProgMeasurable f u
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>TopologicalSpace ι<VAR>TopologicalSpace.MetrizableSpace ι<VAR>SecondCountableTopology ι<VAR>MeasurableSpace ι<VAR>OpensMeasurableSpace ι<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>h : MeasureTheory.Adapted f u<VAR>hu_cont : ∀ (ω : Ω), Continuous fun i => u i ω<GOAL>MeasureTheory.ProgMeasurable f u
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>Preorder ι<VAR>u : ι → Ω → β<VAR>f : MeasureTheory.Filtration ι m<VAR>TopologicalSpace ι<VAR>DiscreteTopology ι<VAR>SecondCountableTopology ι<VAR>MeasurableSpace ι<VAR>OpensMeasurableSpace ι<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>h : MeasureTheory.Adapted f u<GOAL>MeasureTheory.ProgMeasurable f u
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>f : MeasureTheory.Filtration ℕ m<VAR>u : ℕ → Ω → β<VAR>hu : MeasureTheory.Adapted f fun n => u (n + 1)<VAR>hu0 : MeasureTheory.StronglyMeasurable (u 0)<GOAL>MeasureTheory.Adapted f u
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>hκη : κ ≤ η<VAR>a : α<VAR>x : γ<GOAL>0 ≤ κ.rnDerivAux η a x
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>ProbabilityTheory.IsFiniteKernel η<VAR>hκη : κ ≤ η<VAR>a : α<GOAL>κ.rnDerivAux η a ≤ᵐ[η a] 1
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<GOAL>Measurable fun p => κ.rnDerivAux η p.1 p.2
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>a : α<GOAL>Measurable fun x => κ.rnDerivAux η a x
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ∂(κ + η) a = (κ a) s
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<GOAL>((κ + η).withDensity fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal) = κ
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>ProbabilityTheory.IsFiniteKernel η<GOAL>((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) = η
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : ProbabilityTheory.Kernel α γ<VAR>a : α<VAR>x : γ<GOAL>x ∈ κ.mutuallySingularSetSlice η a ↔ 1 ≤ κ.rnDerivAux (κ + η) a x