ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : MeasureTheory.Measure Ω<VAR>μ : MeasureTheory.Measure E<VAR>F : Type u_3<VAR>MeasurableSpace F<VAR>ν : MeasureTheory.Measure F<VAR>MeasureTheory.IsFiniteMeasure ℙ<VAR>MeasureTheory.SigmaFinite ν<VAR>X : Ω → E<VAR>MeasureTheory.HasPDF X ℙ μ<VAR>hX : AEMeasurable X ℙ<VAR>g : E → F<VAR>hg : MeasureTheory.Measure.QuasiMeasurePreserving g μ ν<GOAL>MeasureTheory.HasPDF (g ∘ X) ℙ ν
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>ℙ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure ℙ<VAR>X : Ω → ℝ<VAR>hX : AEMeasurable X ℙ<GOAL>MeasureTheory.HasPDF X ℙ MeasureTheory.volume ↔ MeasureTheory.Measure.map X ℙ ≪ MeasureTheory.volume
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>ℙ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure ℙ<VAR>X : Ω → ℝ<GOAL>MeasureTheory.HasPDF X ℙ MeasureTheory.volume ↔ AEMeasurable X ℙ ∧ MeasureTheory.Measure.map X ℙ ≪ MeasureTheory.volume
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>ℙ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure ℙ<VAR>X : Ω → ℝ<VAR>MeasureTheory.HasPDF X ℙ MeasureTheory.volume<GOAL>∫ (x : ℝ), x * (MeasureTheory.pdf X ℙ MeasureTheory.volume x).toReal = ∫ (x : Ω), X x ∂ℙ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>ℙ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure ℙ<VAR>X : Ω → ℝ<VAR>f : ℝ → ℝ<VAR>g : ℝ → ℝ≥0∞<VAR>hg : MeasureTheory.pdf X ℙ MeasureTheory.volume =ᵐ[MeasureTheory.volume] g<VAR>hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤<GOAL>MeasureTheory.HasFiniteIntegral (fun x => f x * (MeasureTheory.pdf X ℙ MeasureTheory.volume x).toReal) MeasureTheory.volume
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : MeasureTheory.Measure Ω<VAR>μ : MeasureTheory.Measure E<VAR>F : Type u_3<VAR>MeasurableSpace F<VAR>ν : MeasureTheory.Measure F<VAR>X : Ω → E<VAR>Y : Ω → F<VAR>MeasureTheory.IsFiniteMeasure ℙ<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>MeasureTheory.HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)<GOAL>ProbabilityTheory.IndepFun X Y ℙ ↔ MeasureTheory.pdf (fun ω => (X ω, Y ω)) ℙ (μ.prod ν) =ᵐ[μ.prod ν] fun z => MeasureTheory.pdf X ℙ μ z.1 * MeasureTheory.pdf Y ℙ ν z.2
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>m0 : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μα : MeasureTheory.Measure α<VAR>t : Set Ω<VAR>h_indep : ProbabilityTheory.Kernel.IndepSet t t κ μα<GOAL>∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤
<VAR>Ω : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>t : Set Ω<VAR>h_indep : ProbabilityTheory.IndepSet t t μ<GOAL>μ t = 0 ∨ μ t = 1 ∨ μ t = ⊤
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>m0 : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μα : MeasureTheory.Measure α<VAR>∀ (a : α), MeasureTheory.IsFiniteMeasure (κ a)<VAR>t : Set Ω<VAR>h_indep : ProbabilityTheory.Kernel.IndepSet t t κ μα<GOAL>∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1
<VAR>Ω : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>t : Set Ω<VAR>h_indep : ProbabilityTheory.IndepSet t t μ<GOAL>μ t = 0 ∨ μ t = 1
<VAR>Ω : Type u_2<VAR>m m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm : m ≤ m0<VAR>hμ : MeasureTheory.IsFiniteMeasure μ<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>h_indep : ProbabilityTheory.CondIndepSet m hm t t μ<GOAL>∀ᵐ (ω : Ω) ∂μ, (μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μα : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.Kernel.iIndep s κ μα<VAR>t : Set ι<GOAL>ProbabilityTheory.Kernel.Indep (⨆ n ∈ t, s n) (⨆ n ∈ tᶜ, s n) κ μα
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iIndep s μ<VAR>t : Set ι<GOAL>ProbabilityTheory.Indep (⨆ n ∈ t, s n) (⨆ n ∈ tᶜ, s n) μ
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm : m ≤ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iCondIndep m hm s μ<VAR>t : Set ι<GOAL>ProbabilityTheory.CondIndep m (⨆ n ∈ t, s n) (⨆ n ∈ tᶜ, s n) hm μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μα : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.Kernel.iIndep s κ μα<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>t : Set ι<VAR>ht : p t<GOAL>ProbabilityTheory.Kernel.Indep (⨆ n ∈ t, s n) (Filter.limsup s f) κ μα
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iIndep s μ<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>t : Set ι<VAR>ht : p t<GOAL>ProbabilityTheory.Indep (⨆ n ∈ t, s n) (Filter.limsup s f) μ
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm : m ≤ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iCondIndep m hm s μ<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>t : Set ι<VAR>ht : p t<GOAL>ProbabilityTheory.CondIndep m (⨆ n ∈ t, s n) (Filter.limsup s f) hm μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μα : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<GOAL>∀ {α_1 : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : α_1 → Set ι}, (∀ (n : ι), s n ≤ m0) → ProbabilityTheory.Kernel.iIndep s κ μα → (∀ (t : Set ι), p t → tᶜ ∈ f) → Directed (fun x x_1 => x ≤ x_1) ns → (∀ (a : α_1), p (ns a)) → ProbabilityTheory.Kernel.Indep (⨆ a, ⨆ n ∈ ns a, s n) (Filter.limsup s f) κ μα
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iIndep s μ<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<GOAL>ProbabilityTheory.Indep (⨆ a, ⨆ n ∈ ns a, s n) (Filter.limsup s f) μ
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm : m ≤ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iCondIndep m hm s μ<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<GOAL>ProbabilityTheory.CondIndep m (⨆ a, ⨆ n ∈ ns a, s n) (Filter.limsup s f) hm μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μα : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<GOAL>∀ {α_1 : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : α_1 → Set ι}, (∀ (n : ι), s n ≤ m0) → ProbabilityTheory.Kernel.iIndep s κ μα → (∀ (t : Set ι), p t → tᶜ ∈ f) → Directed (fun x x_1 => x ≤ x_1) ns → (∀ (a : α_1), p (ns a)) → (∀ (n : ι), ∃ a, n ∈ ns a) → ProbabilityTheory.Kernel.Indep (⨆ n, s n) (Filter.limsup s f) κ μα
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iIndep s μ<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<GOAL>ProbabilityTheory.Indep (⨆ n, s n) (Filter.limsup s f) μ
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm : m ≤ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iCondIndep m hm s μ<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<GOAL>ProbabilityTheory.CondIndep m (⨆ n, s n) (Filter.limsup s f) hm μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μα : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<GOAL>∀ {α_1 : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : α_1 → Set ι}, (∀ (n : ι), s n ≤ m0) → ProbabilityTheory.Kernel.iIndep s κ μα → (∀ (t : Set ι), p t → tᶜ ∈ f) → Directed (fun x x_1 => x ≤ x_1) ns → (∀ (a : α_1), p (ns a)) → (∀ (n : ι), ∃ a, n ∈ ns a) → ProbabilityTheory.Kernel.Indep (Filter.limsup s f) (Filter.limsup s f) κ μα
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iIndep s μ<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<GOAL>ProbabilityTheory.Indep (Filter.limsup s f) (Filter.limsup s f) μ
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm : m ≤ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iCondIndep m hm s μ<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<GOAL>ProbabilityTheory.CondIndep m (Filter.limsup s f) (Filter.limsup s f) hm μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μα : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<GOAL>∀ {α_1 : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : α_1 → Set ι}, (∀ (n : ι), s n ≤ m0) → ProbabilityTheory.Kernel.iIndep s κ μα → (∀ (t : Set ι), p t → tᶜ ∈ f) → Directed (fun x x_1 => x ≤ x_1) ns → (∀ (a : α_1), p (ns a)) → (∀ (n : ι), ∃ a, n ∈ ns a) → ∀ {t : Set Ω}, MeasurableSet t → ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iIndep s μ<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<VAR>t : Set Ω<VAR>ht_tail : MeasurableSet t<GOAL>μ t = 0 ∨ μ t = 1
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm : m ≤ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iCondIndep m hm s μ<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<VAR>t : Set Ω<VAR>ht_tail : MeasurableSet t<GOAL>∀ᵐ (ω : Ω) ∂μ, (μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μα : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>SemilatticeSup ι<VAR>NoMaxOrder ι<VAR>Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.Kernel.iIndep s κ μα<GOAL>ProbabilityTheory.Kernel.Indep (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) κ μα
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>SemilatticeSup ι<VAR>NoMaxOrder ι<VAR>Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iIndep s μ<GOAL>ProbabilityTheory.Indep (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) μ
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>SemilatticeSup ι<VAR>NoMaxOrder ι<VAR>Nonempty ι<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm : m ≤ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iCondIndep m hm s μ<GOAL>ProbabilityTheory.CondIndep m (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) hm μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μα : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>SemilatticeSup ι<VAR>NoMaxOrder ι<VAR>Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.Kernel.iIndep s κ μα<VAR>t : Set Ω<VAR>ht_tail : MeasurableSet t<GOAL>∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>SemilatticeSup ι<VAR>NoMaxOrder ι<VAR>Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iIndep s μ<VAR>t : Set Ω<VAR>ht_tail : MeasurableSet t<GOAL>μ t = 0 ∨ μ t = 1
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>SemilatticeSup ι<VAR>NoMaxOrder ι<VAR>Nonempty ι<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm : m ≤ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iCondIndep m hm s μ<VAR>t : Set Ω<VAR>ht_tail : MeasurableSet t<GOAL>∀ᵐ (ω : Ω) ∂μ, (μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μα : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>SemilatticeInf ι<VAR>NoMinOrder ι<VAR>Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.Kernel.iIndep s κ μα<GOAL>ProbabilityTheory.Kernel.Indep (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) κ μα
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>SemilatticeInf ι<VAR>NoMinOrder ι<VAR>Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iIndep s μ<GOAL>ProbabilityTheory.Indep (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) μ
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>SemilatticeInf ι<VAR>NoMinOrder ι<VAR>Nonempty ι<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm : m ≤ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iCondIndep m hm s μ<GOAL>ProbabilityTheory.CondIndep m (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) hm μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μα : MeasureTheory.Measure α<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>SemilatticeInf ι<VAR>NoMinOrder ι<VAR>Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.Kernel.iIndep s κ μα<VAR>t : Set Ω<VAR>ht_tail : MeasurableSet t<GOAL>∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>SemilatticeInf ι<VAR>NoMinOrder ι<VAR>Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iIndep s μ<VAR>t : Set Ω<VAR>ht_tail : MeasurableSet t<GOAL>μ t = 0 ∨ μ t = 1
<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>SemilatticeInf ι<VAR>NoMinOrder ι<VAR>Nonempty ι<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm : m ≤ m0<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : ProbabilityTheory.iCondIndep m hm s μ<VAR>t : Set Ω<VAR>ht_tail : MeasurableSet t<GOAL>∀ᵐ (ω : Ω) ∂μ, (μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1
<VAR>E : Type u_1<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>Ω : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E}, μ s ≠ 0 → μ s ≠ ⊤ → MeasureTheory.pdf.IsUniform X s ℙ μ → AEMeasurable X ℙ
<VAR>E : Type u_1<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>Ω : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E}, MeasureTheory.pdf.IsUniform X s ℙ μ → MeasureTheory.Measure.map X ℙ ≪ μ
<VAR>E : Type u_1<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>Ω : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E}, μ s ≠ 0 → μ s ≠ ⊤ → MeasureTheory.pdf.IsUniform X s ℙ μ → ∀ {A : Set E}, MeasurableSet A → ℙ (X ⁻¹' A) = μ (s ∩ A) / μ s
<VAR>E : Type u_1<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>Ω : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E}, μ s ≠ 0 → μ s ≠ ⊤ → MeasureTheory.pdf.IsUniform X s ℙ μ → MeasureTheory.IsProbabilityMeasure ℙ
<VAR>E : Type u_1<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>Ω : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E}, MeasureTheory.pdf.IsUniform X (MeasureTheory.toMeasurable μ s) ℙ μ ↔ MeasureTheory.pdf.IsUniform X s ℙ μ
<VAR>E : Type u_1<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>Ω : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E}, MeasureTheory.pdf.IsUniform X s ℙ μ → MeasureTheory.pdf.IsUniform X (MeasureTheory.toMeasurable μ s) ℙ μ
<VAR>E : Type u_1<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>Ω : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E}, μ s ≠ 0 → μ s ≠ ⊤ → MeasureTheory.pdf.IsUniform X s ℙ μ → MeasureTheory.HasPDF X ℙ μ
<VAR>E : Type u_1<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>Ω : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E}, MeasureTheory.pdf.IsUniform X s ℙ μ → μ s = 0 ∨ μ s = ⊤ → MeasureTheory.pdf X ℙ μ =ᵐ[μ] 0
<VAR>E : Type u_1<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>Ω : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E}, MeasurableSet s → MeasureTheory.pdf.IsUniform X s ℙ μ → MeasureTheory.pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • 1)
<VAR>E : Type u_1<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>Ω : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E}, MeasurableSet s → MeasureTheory.pdf.IsUniform X s ℙ μ → (fun x_1 => (MeasureTheory.pdf X ℙ μ x_1).toReal) =ᵐ[μ] fun x => (s.indicator ((μ s)⁻¹ • 1) x).toReal
<VAR>Ω : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {s : Set ℝ}, IsCompact s → MeasureTheory.pdf.IsUniform X s ℙ MeasureTheory.volume → MeasureTheory.Integrable (fun x_1 => x_1 * (MeasureTheory.pdf X ℙ MeasureTheory.volume x_1).toReal) MeasureTheory.volume
<VAR>Ω : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {s : Set ℝ}, MeasureTheory.pdf.IsUniform X s ℙ MeasureTheory.volume → ∫ (x : Ω), X x ∂ℙ = (MeasureTheory.volume s)⁻¹.toReal * ∫ (x : ℝ) in s, x
<VAR>E : Type u_1<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>s : Set E<GOAL>MeasureTheory.pdf.IsUniform id s (ProbabilityTheory.cond μ s) μ
<VAR>E : Type u_1<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>Ω : Type u_2<GOAL>∀ {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E}, MeasurableSet s → MeasureTheory.pdf.IsUniform X s ℙ μ → (fun x => MeasureTheory.pdf.uniformPDF s x μ) =ᵐ[μ] MeasureTheory.pdf X ℙ μ
<VAR>E : Type u_1<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>s : Set E<VAR>x : E<GOAL>MeasureTheory.pdf.uniformPDF s x μ = if x ∈ s then (μ s)⁻¹ else 0
<VAR>α : Type u_1<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>a : α<GOAL>(PMF.uniformOfFinset s hs) a = if a ∈ s then (↑s.card)⁻¹ else 0
<VAR>α : Type u_1<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>a : α<VAR>ha : a ∈ s<GOAL>(PMF.uniformOfFinset s hs) a = (↑s.card)⁻¹
<VAR>α : Type u_1<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>a : α<VAR>ha : a ∉ s<GOAL>(PMF.uniformOfFinset s hs) a = 0
<VAR>α : Type u_1<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>(PMF.uniformOfFinset s hs).support = ↑s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>a : α<GOAL>a ∈ (PMF.uniformOfFinset s hs).support ↔ a ∈ s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>t : Set α<GOAL>(PMF.uniformOfFinset s hs).toOuterMeasure t = ↑(Finset.filter (fun x => x ∈ t) s).card / ↑s.card
<VAR>α : Type u_1<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>t : Set α<VAR>MeasurableSpace α<VAR>ht : MeasurableSet t<GOAL>(PMF.uniformOfFinset s hs).toMeasure t = ↑(Finset.filter (fun x => x ∈ t) s).card / ↑s.card
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>a : α<GOAL>(PMF.uniformOfFintype α) a = (↑(Fintype.card α))⁻¹
<VAR>α : Type u_4<VAR>Fintype α<VAR>Nonempty α<GOAL>(PMF.uniformOfFintype α).support = ⊤
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>a : α<GOAL>a ∈ (PMF.uniformOfFintype α).support
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>s : Set α<GOAL>(PMF.uniformOfFintype α).toOuterMeasure s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<VAR>s : Set α<VAR>MeasurableSpace α<VAR>hs : MeasurableSet s<GOAL>(PMF.uniformOfFintype α).toMeasure s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>hs : s ≠ 0<VAR>a : α<GOAL>(PMF.ofMultiset s hs) a = ↑(Multiset.count a s) / ↑(Multiset.card s)
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>hs : s ≠ 0<GOAL>(PMF.ofMultiset s hs).support = ↑s.toFinset
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>hs : s ≠ 0<VAR>a : α<GOAL>a ∈ (PMF.ofMultiset s hs).support ↔ a ∈ s.toFinset
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>hs : s ≠ 0<VAR>a : α<VAR>ha : a ∉ s<GOAL>(PMF.ofMultiset s hs) a = 0