ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' m₁ mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>SemilatticeInf ι<VAR>m : ι → MeasurableSpace Ω<VAR>h_indep : ∀ (i : ι), ProbabilityTheory.CondIndep m' (m i) m₁ hm' μ<VAR>h_le : ∀ (i : ι), m i ≤ mΩ<VAR>h_le' : m₁ ≤ mΩ<VAR>hm : Antitone m<GOAL>ProbabilityTheory.CondIndep m' (⨆ i, m i) m₁ hm' μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>π : ι → Set (Set Ω)<VAR>a : ι<VAR>S : Finset ι<VAR>hp_ind : ProbabilityTheory.iCondIndepSets m' hm' π μ<VAR>haS : a ∉ S<GOAL>ProbabilityTheory.CondIndepSets m' hm' (piiUnionInter π ↑S) (π a) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>m : ι → MeasurableSpace Ω<VAR>h_le : ∀ (i : ι), m i ≤ mΩ<VAR>π : ι → Set (Set Ω)<VAR>h_pi : ∀ (n : ι), IsPiSystem (π n)<VAR>h_generate : ∀ (i : ι), m i = MeasurableSpace.generateFrom (π i)<VAR>h_ind : ProbabilityTheory.iCondIndepSets m' hm' π μ<GOAL>ProbabilityTheory.iCondIndep m' hm' m μ
<VAR>Ω : Type u_1<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s t : Set Ω<VAR>S T : Set (Set Ω)<VAR>hs : s ∈ S<VAR>ht : t ∈ T<VAR>hs_meas : MeasurableSet s<VAR>ht_meas : MeasurableSet t<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h_indep : ProbabilityTheory.CondIndepSets m' hm' S T μ<GOAL>ProbabilityTheory.CondIndepSet m' hm' s t μ
<VAR>Ω : Type u_1<VAR>m' m₁ m₂ mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>h_indep : ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ<VAR>s t : Set Ω<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>ProbabilityTheory.CondIndepSet m' hm' s t μ
<VAR>Ω : Type u_1<VAR>m' m₁ m₂ mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ ↔ ∀ (s t : Set Ω), MeasurableSet s → MeasurableSet t → ProbabilityTheory.CondIndepSet m' hm' s t μ
<VAR>Ω : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>ProbabilityTheory.CondIndepFun m' hm' f g μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω => 1|m'] =ᵐ[μ] fun ω => (μ[(f ⁻¹' s).indicator fun ω => 1|m']) ω * (μ[(g ⁻¹' t).indicator fun ω => 1|m']) ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : ι → Type u_5<VAR>m : (x : ι) → MeasurableSpace (β x)<VAR>f : (i : ι) → Ω → β i<VAR>hf : ∀ (i : ι), Measurable (f i)<GOAL>ProbabilityTheory.iCondIndepFun m' hm' m f μ ↔ ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)}, (∀ i ∈ S, MeasurableSet (sets i)) → μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω => 1|m'] =ᵐ[μ] ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>ProbabilityTheory.CondIndepFun m' hm' f g μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → ProbabilityTheory.CondIndepSet m' hm' (f ⁻¹' s) (g ⁻¹' t) μ
<VAR>Ω : Type u_1<VAR>β : Type u_3<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>∀ {x : MeasurableSpace β} {f g : Ω → β}, ProbabilityTheory.CondIndepFun m' hm' f g μ → ProbabilityTheory.CondIndepFun m' hm' g f μ
<VAR>Ω : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>_mβ : MeasurableSpace β<VAR>_mβ' : MeasurableSpace β'<VAR>_mγ : MeasurableSpace γ<VAR>_mγ' : MeasurableSpace γ'<VAR>φ : β → γ<VAR>ψ : β' → γ'<VAR>hfg : ProbabilityTheory.CondIndepFun m' hm' f g μ<VAR>hφ : Measurable φ<VAR>hψ : Measurable ψ<GOAL>ProbabilityTheory.CondIndepFun m' hm' (φ ∘ f) (ψ ∘ g) μ
<VAR>Ω : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>_mβ : MeasurableSpace β<VAR>_mβ' : MeasurableSpace β'<VAR>Neg β'<VAR>MeasurableNeg β'<VAR>hfg : ProbabilityTheory.CondIndepFun m' hm' f g μ<GOAL>ProbabilityTheory.CondIndepFun m' hm' f (-g) μ
<VAR>Ω : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>_mβ : MeasurableSpace β<VAR>_mβ' : MeasurableSpace β'<VAR>Neg β<VAR>MeasurableNeg β<VAR>hfg : ProbabilityTheory.CondIndepFun m' hm' f g μ<GOAL>ProbabilityTheory.CondIndepFun m' hm' (-f) g μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : ι → Type u_5<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>Subsingleton ι<GOAL>ProbabilityTheory.iCondIndepFun m' hm' m f μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : ι → Type u_6<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>S T : Finset ι<VAR>hST : Disjoint S T<VAR>hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' m f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<GOAL>ProbabilityTheory.CondIndepFun m' hm' (fun a i => f (↑i) a) (fun a i => f (↑i) a) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : ι → Type u_6<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' m f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<GOAL>ProbabilityTheory.CondIndepFun m' hm' (fun a => (f i a, f j a)) (f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : ι → Type u_5<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>h_indep : ProbabilityTheory.iCondIndepFun m' hm' m f μ<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>i j k l : ι<VAR>hik : i ≠ k<VAR>hil : i ≠ l<VAR>hjk : j ≠ k<VAR>hjl : j ≠ l<GOAL>ProbabilityTheory.CondIndepFun m' hm' (fun a => (f i a, f j a)) (fun a => (f k a, f l a)) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : Type u_5<VAR>m : MeasurableSpace β<VAR>Add β<VAR>MeasurableAdd₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun x => m) f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<GOAL>ProbabilityTheory.CondIndepFun m' hm' (f i + f j) (f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : Type u_5<VAR>m : MeasurableSpace β<VAR>Mul β<VAR>MeasurableMul₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun x => m) f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<GOAL>ProbabilityTheory.CondIndepFun m' hm' (f i * f j) (f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : Type u_5<VAR>m : MeasurableSpace β<VAR>Add β<VAR>MeasurableAdd₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun x => m) f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hij : i ≠ j<VAR>hik : i ≠ k<GOAL>ProbabilityTheory.CondIndepFun m' hm' (f i) (f j + f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : Type u_5<VAR>m : MeasurableSpace β<VAR>Mul β<VAR>MeasurableMul₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun x => m) f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hij : i ≠ j<VAR>hik : i ≠ k<GOAL>ProbabilityTheory.CondIndepFun m' hm' (f i) (f j * f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : Type u_5<VAR>m : MeasurableSpace β<VAR>Mul β<VAR>MeasurableMul₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun x => m) f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k l : ι<VAR>hik : i ≠ k<VAR>hil : i ≠ l<VAR>hjk : j ≠ k<VAR>hjl : j ≠ l<GOAL>ProbabilityTheory.CondIndepFun m' hm' (f i * f j) (f k * f l) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : Type u_5<VAR>m : MeasurableSpace β<VAR>Add β<VAR>MeasurableAdd₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun x => m) f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k l : ι<VAR>hik : i ≠ k<VAR>hil : i ≠ l<VAR>hjk : j ≠ k<VAR>hjl : j ≠ l<GOAL>ProbabilityTheory.CondIndepFun m' hm' (f i + f j) (f k + f l) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : Type u_5<VAR>m : MeasurableSpace β<VAR>Sub β<VAR>MeasurableSub₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun x => m) f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<GOAL>ProbabilityTheory.CondIndepFun m' hm' (f i - f j) (f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : Type u_5<VAR>m : MeasurableSpace β<VAR>Div β<VAR>MeasurableDiv₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun x => m) f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<GOAL>ProbabilityTheory.CondIndepFun m' hm' (f i / f j) (f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : Type u_5<VAR>m : MeasurableSpace β<VAR>Div β<VAR>MeasurableDiv₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun x => m) f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hij : i ≠ j<VAR>hik : i ≠ k<GOAL>ProbabilityTheory.CondIndepFun m' hm' (f i) (f j / f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : Type u_5<VAR>m : MeasurableSpace β<VAR>Sub β<VAR>MeasurableSub₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun x => m) f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hij : i ≠ j<VAR>hik : i ≠ k<GOAL>ProbabilityTheory.CondIndepFun m' hm' (f i) (f j - f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : Type u_5<VAR>m : MeasurableSpace β<VAR>Sub β<VAR>MeasurableSub₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun x => m) f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k l : ι<VAR>hik : i ≠ k<VAR>hil : i ≠ l<VAR>hjk : j ≠ k<VAR>hjl : j ≠ l<GOAL>ProbabilityTheory.CondIndepFun m' hm' (f i - f j) (f k - f l) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : Type u_5<VAR>m : MeasurableSpace β<VAR>Div β<VAR>MeasurableDiv₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iCondIndepFun m' hm' (fun x => m) f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k l : ι<VAR>hik : i ≠ k<VAR>hil : i ≠ l<VAR>hjk : j ≠ k<VAR>hjl : j ≠ l<GOAL>ProbabilityTheory.CondIndepFun m' hm' (f i / f j) (f k / f l) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : Type u_5<VAR>m : MeasurableSpace β<VAR>CommMonoid β<VAR>MeasurableMul₂ β<VAR>f : ι → Ω → β<VAR>hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' (fun x => m) f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∉ s<GOAL>ProbabilityTheory.CondIndepFun m' hm' (∏ j ∈ s, f j) (f i) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : Type u_5<VAR>m : MeasurableSpace β<VAR>AddCommMonoid β<VAR>MeasurableAdd₂ β<VAR>f : ι → Ω → β<VAR>hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' (fun x => m) f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∉ s<GOAL>ProbabilityTheory.CondIndepFun m' hm' (∑ j ∈ s, f j) (f i) μ
<VAR>Ω : Type u_1<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : Type u_5<VAR>m : MeasurableSpace β<VAR>AddCommMonoid β<VAR>MeasurableAdd₂ β<VAR>f : ℕ → Ω → β<VAR>hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' (fun x => m) f μ<VAR>hf_meas : ∀ (i : ℕ), Measurable (f i)<VAR>n : ℕ<GOAL>ProbabilityTheory.CondIndepFun m' hm' (∑ j ∈ Finset.range n, f j) (f n) μ
<VAR>Ω : Type u_1<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>β : Type u_5<VAR>m : MeasurableSpace β<VAR>CommMonoid β<VAR>MeasurableMul₂ β<VAR>f : ℕ → Ω → β<VAR>hf_Indep : ProbabilityTheory.iCondIndepFun m' hm' (fun x => m) f μ<VAR>hf_meas : ∀ (i : ℕ), Measurable (f i)<VAR>n : ℕ<GOAL>ProbabilityTheory.CondIndepFun m' hm' (∏ j ∈ Finset.range n, f j) (f n) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>m' mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>Zero β<VAR>One β<VAR>m : MeasurableSpace β<VAR>s : ι → Set Ω<VAR>hs : ProbabilityTheory.iCondIndepSet m' hm' s μ<GOAL>ProbabilityTheory.iCondIndepFun m' hm' (fun _n => m) (fun n => (s n).indicator fun _ω => 1) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<VAR>n : ℕ<VAR>s : Set α<VAR>hs : s ∈ memPartition t n<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<VAR>n : ℕ<VAR>a : α<GOAL>MeasurableSet (memPartitionSet t n a)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<VAR>n : ℕ<GOAL>∀ (m_1 : MeasurableSpace ↑(memPartition t n)), Measurable fun a => ⟨memPartitionSet t n a, ⋯⟩
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<VAR>n : ℕ<GOAL>Measurable (memPartitionSet t n)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<GOAL>⨆ n, ↑(ProbabilityTheory.partitionFiltration ht) n = MeasurableSpace.generateFrom (Set.range t)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<VAR>ht_range : MeasurableSpace.generateFrom (Set.range t) = m<GOAL>⨆ n, ↑(ProbabilityTheory.partitionFiltration ht) n = m
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<VAR>s : Set α<VAR>hs : s ∈ MeasurableSpace.countablePartition α n<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<VAR>t : α<GOAL>MeasurableSet (MeasurableSpace.countablePartitionSet n t)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<VAR>m : MeasurableSpace ↑(MeasurableSpace.countablePartition α n)<GOAL>Measurable fun a => ⟨MeasurableSpace.countablePartitionSet n a, ⋯⟩
<VAR>α : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<VAR>n : ℕ<GOAL>Measurable (MeasurableSpace.countablePartitionSet n)
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>MeasurableSpace.CountablyGenerated α<GOAL>⨆ n, ↑(ProbabilityTheory.countableFiltration α) n = m
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>Ω : Type u_7<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<GOAL>∀ {x : MeasurableSpace α} [inst : MeasurableSpace β] (Y : α → Ω) (X : α → β) (μ : MeasureTheory.Measure α) [inst_1 : MeasureTheory.IsFiniteMeasure μ], ProbabilityTheory.condDistrib Y X μ = (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ).condKernel
<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>MeasurableSingletonClass β<VAR>hY : Measurable Y<VAR>x : β<VAR>hX : (MeasureTheory.Measure.map X μ) {x} ≠ 0<VAR>s : Set Ω<GOAL>((ProbabilityTheory.condDistrib Y X μ) x) s = ((MeasureTheory.Measure.map X μ) {x})⁻¹ * (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) ({x} ×ˢ 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>hs : MeasurableSet s<GOAL>Measurable fun a => ((ProbabilityTheory.condDistrib Y X μ) (X a)) s
<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 : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)<GOAL>(∀ᵐ (a : β) ∂MeasureTheory.Measure.map X μ, MeasureTheory.Integrable (fun ω => f (a, ω)) ((ProbabilityTheory.condDistrib Y X μ) a)) ∧ MeasureTheory.Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂(ProbabilityTheory.condDistrib Y X μ) a) (MeasureTheory.Measure.map X μ) ↔ MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y 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 : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)<GOAL>MeasureTheory.AEStronglyMeasurable (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 : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)<GOAL>MeasureTheory.AEStronglyMeasurable (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>hX : AEMeasurable X μ<VAR>hY : AEMeasurable Y μ<VAR>hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)<GOAL>MeasureTheory.AEStronglyMeasurable' (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>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>mα : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>hX : Measurable X<VAR>hY : Measurable Y<VAR>κ : ProbabilityTheory.Kernel β Ω<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>hκ : MeasureTheory.Measure.map (fun x => (X x, Y x)) μ = MeasureTheory.Measure.map X μ ⊗ₘ κ<GOAL>∀ᵐ (x : β) ∂MeasureTheory.Measure.map X μ, κ x = (ProbabilityTheory.condDistrib Y X μ) x
<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 : AEMeasurable X μ<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.Integrable (fun a => (((ProbabilityTheory.condDistrib Y X μ) (X a)) s).toReal) μ
<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>∀ᵐ (b : β) ∂MeasureTheory.Measure.map X μ, MeasureTheory.Integrable (fun ω => f (b, ω)) ((ProbabilityTheory.condDistrib Y X μ) b)