ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<VAR>s t : Set Ω<VAR>hs_meas : MeasurableSet s<VAR>ht_meas : MeasurableSet t<VAR>μ : MeasureTheory.Measure Ω := by volume_tac<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>ProbabilityTheory.IndepSet s t μ ↔ ProbabilityTheory.IndepSets {s} {t} μ
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<VAR>s t : Set Ω<VAR>hs_meas : MeasurableSet s<VAR>ht_meas : MeasurableSet t<VAR>μ : MeasureTheory.Measure Ω := by volume_tac<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>ProbabilityTheory.IndepSet s t μ ↔ μ (s ∩ t) = μ s * μ t
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<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 Ω := by volume_tac<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>h_indep : ProbabilityTheory.IndepSets S T μ<GOAL>ProbabilityTheory.IndepSet s t μ
<VAR>Ω : Type u_1<VAR>m₁ m₂ _mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>h_indep : ProbabilityTheory.Indep m₁ m₂ μ<VAR>s t : Set Ω<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>ProbabilityTheory.IndepSet s t μ
<VAR>Ω : Type u_1<VAR>m₁ m₂ _mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<GOAL>ProbabilityTheory.Indep m₁ m₂ μ ↔ ∀ (s t : Set Ω), MeasurableSet s → MeasurableSet t → ProbabilityTheory.IndepSet s t μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f : ι → Set Ω<GOAL>ProbabilityTheory.iIndep (fun i => MeasurableSpace.comap (fun x => x ∈ f i) ⊤) μ ↔ ProbabilityTheory.iIndepSet f μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>s : ι → Set Ω<GOAL>ProbabilityTheory.iIndepSets (fun i => {s i}) μ ↔ ∀ (t : Finset ι), μ (⋂ i ∈ t, s i) = ∏ i ∈ t, μ (s i)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>f : ι → Set Ω<VAR>hf : ∀ (i : ι), MeasurableSet (f i)<GOAL>ProbabilityTheory.iIndepSet f μ ↔ ProbabilityTheory.iIndepSets (fun i => {f i}) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>f : ι → Set Ω<VAR>hf : ∀ (i : ι), MeasurableSet (f i)<GOAL>ProbabilityTheory.iIndepSet f μ ↔ ∀ (s : Finset ι), μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>π : ι → Set (Set Ω)<VAR>f : ι → Set Ω<VAR>hfπ : ∀ (i : ι), f i ∈ π i<VAR>hf : ∀ (i : ι), MeasurableSet (f i)<VAR>hπ : ProbabilityTheory.iIndepSets π μ<GOAL>ProbabilityTheory.iIndepSet f μ
<VAR>Ω : Type u_1<VAR>β : Type u_6<VAR>β' : Type u_7<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<GOAL>ProbabilityTheory.IndepFun f g μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>ι : Type u_10<VAR>β : ι → Type u_11<VAR>m : (x : ι) → MeasurableSpace (β x)<VAR>f : (i : ι) → Ω → β i<GOAL>ProbabilityTheory.iIndepFun m f μ ↔ ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)}, (∀ i ∈ S, MeasurableSet (sets i)) → μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i)
<VAR>Ω : Type u_1<VAR>β : Type u_6<VAR>β' : Type u_7<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>ProbabilityTheory.IndepFun f g μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → ProbabilityTheory.IndepSet (f ⁻¹' s) (g ⁻¹' t) μ
<VAR>Ω : Type u_1<VAR>β : Type u_6<VAR>β' : Type u_7<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>ProbabilityTheory.IndepFun f g μ ↔ MeasureTheory.Measure.map (fun ω => (f ω, g ω)) μ = (MeasureTheory.Measure.map f μ).prod (MeasureTheory.Measure.map g μ)
<VAR>Ω : Type u_1<VAR>β : Type u_6<VAR>β' : Type u_7<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f : Ω → β<VAR>g : Ω → β'<GOAL>∀ {x : MeasurableSpace β} {x_1 : MeasurableSpace β'}, ProbabilityTheory.IndepFun f g μ → ProbabilityTheory.IndepFun g f μ
<VAR>Ω : Type u_1<VAR>β : Type u_6<VAR>β' : Type u_7<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>f' : Ω → β<VAR>g' : Ω → β'<VAR>hfg : ProbabilityTheory.IndepFun f g μ<VAR>hf : f =ᵐ[μ] f'<VAR>hg : g =ᵐ[μ] g'<GOAL>ProbabilityTheory.IndepFun f' g' μ
<VAR>Ω : Type u_1<VAR>β : Type u_6<VAR>β' : Type u_7<VAR>γ : Type u_8<VAR>γ' : Type u_9<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>_mβ : MeasurableSpace β<VAR>_mβ' : MeasurableSpace β'<VAR>_mγ : MeasurableSpace γ<VAR>_mγ' : MeasurableSpace γ'<VAR>φ : β → γ<VAR>ψ : β' → γ'<VAR>hfg : ProbabilityTheory.IndepFun f g μ<VAR>hφ : Measurable φ<VAR>hψ : Measurable ψ<GOAL>ProbabilityTheory.IndepFun (φ ∘ f) (ψ ∘ g) μ
<VAR>Ω : Type u_1<VAR>β : Type u_6<VAR>β' : Type u_7<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>_mβ : MeasurableSpace β<VAR>_mβ' : MeasurableSpace β'<VAR>Neg β'<VAR>MeasurableNeg β'<VAR>hfg : ProbabilityTheory.IndepFun f g μ<GOAL>ProbabilityTheory.IndepFun f (-g) μ
<VAR>Ω : Type u_1<VAR>β : Type u_6<VAR>β' : Type u_7<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>_mβ : MeasurableSpace β<VAR>_mβ' : MeasurableSpace β'<VAR>Neg β<VAR>MeasurableNeg β<VAR>hfg : ProbabilityTheory.IndepFun f g μ<GOAL>ProbabilityTheory.IndepFun (-f) g μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : ι → Type u_10<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>Subsingleton ι<GOAL>ProbabilityTheory.iIndepFun m f μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : ι → Type u_10<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>h : ProbabilityTheory.iIndepFun m f μ<GOAL>MeasureTheory.IsProbabilityMeasure μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : ι → Type u_10<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>S T : Finset ι<VAR>hST : Disjoint S T<VAR>hf_Indep : ProbabilityTheory.iIndepFun m f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<GOAL>ProbabilityTheory.IndepFun (fun a i => f (↑i) a) (fun a i => f (↑i) a) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : ι → Type u_10<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>hf_Indep : ProbabilityTheory.iIndepFun m f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<GOAL>ProbabilityTheory.IndepFun (fun a => (f i a, f j a)) (f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : ι → Type u_10<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>h_indep : ProbabilityTheory.iIndepFun 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.IndepFun (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Ω : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_10<VAR>m : MeasurableSpace β<VAR>Mul β<VAR>MeasurableMul₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iIndepFun (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.IndepFun (f i * f j) (f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_10<VAR>m : MeasurableSpace β<VAR>Add β<VAR>MeasurableAdd₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iIndepFun (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.IndepFun (f i + f j) (f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_10<VAR>m : MeasurableSpace β<VAR>Add β<VAR>MeasurableAdd₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iIndepFun (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.IndepFun (f i) (f j + f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_10<VAR>m : MeasurableSpace β<VAR>Mul β<VAR>MeasurableMul₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iIndepFun (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.IndepFun (f i) (f j * f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_10<VAR>m : MeasurableSpace β<VAR>Mul β<VAR>MeasurableMul₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iIndepFun (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.IndepFun (f i * f j) (f k * f l) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_10<VAR>m : MeasurableSpace β<VAR>Add β<VAR>MeasurableAdd₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iIndepFun (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.IndepFun (f i + f j) (f k + f l) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_10<VAR>m : MeasurableSpace β<VAR>Div β<VAR>MeasurableDiv₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iIndepFun (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.IndepFun (f i / f j) (f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_10<VAR>m : MeasurableSpace β<VAR>Sub β<VAR>MeasurableSub₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iIndepFun (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.IndepFun (f i - f j) (f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_10<VAR>m : MeasurableSpace β<VAR>Sub β<VAR>MeasurableSub₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iIndepFun (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.IndepFun (f i) (f j - f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_10<VAR>m : MeasurableSpace β<VAR>Div β<VAR>MeasurableDiv₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iIndepFun (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.IndepFun (f i) (f j / f k) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_10<VAR>m : MeasurableSpace β<VAR>Sub β<VAR>MeasurableSub₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iIndepFun (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.IndepFun (f i - f j) (f k - f l) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_10<VAR>m : MeasurableSpace β<VAR>Div β<VAR>MeasurableDiv₂ β<VAR>f : ι → Ω → β<VAR>hf_indep : ProbabilityTheory.iIndepFun (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.IndepFun (f i / f j) (f k / f l) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_10<VAR>m : MeasurableSpace β<VAR>CommMonoid β<VAR>MeasurableMul₂ β<VAR>f : ι → Ω → β<VAR>hf_Indep : ProbabilityTheory.iIndepFun (fun x => m) f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∉ s<GOAL>ProbabilityTheory.IndepFun (∏ j ∈ s, f j) (f i) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_10<VAR>m : MeasurableSpace β<VAR>AddCommMonoid β<VAR>MeasurableAdd₂ β<VAR>f : ι → Ω → β<VAR>hf_Indep : ProbabilityTheory.iIndepFun (fun x => m) f μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∉ s<GOAL>ProbabilityTheory.IndepFun (∑ j ∈ s, f j) (f i) μ
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_10<VAR>m : MeasurableSpace β<VAR>CommMonoid β<VAR>MeasurableMul₂ β<VAR>f : ℕ → Ω → β<VAR>hf_Indep : ProbabilityTheory.iIndepFun (fun x => m) f μ<VAR>hf_meas : ∀ (i : ℕ), Measurable (f i)<VAR>n : ℕ<GOAL>ProbabilityTheory.IndepFun (∏ j ∈ Finset.range n, f j) (f n) μ
<VAR>Ω : Type u_1<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>β : Type u_10<VAR>m : MeasurableSpace β<VAR>AddCommMonoid β<VAR>MeasurableAdd₂ β<VAR>f : ℕ → Ω → β<VAR>hf_Indep : ProbabilityTheory.iIndepFun (fun x => m) f μ<VAR>hf_meas : ∀ (i : ℕ), Measurable (f i)<VAR>n : ℕ<GOAL>ProbabilityTheory.IndepFun (∑ j ∈ Finset.range n, f j) (f n) μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_6<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>Zero β<VAR>One β<VAR>m : MeasurableSpace β<VAR>s : ι → Set Ω<VAR>hs : ProbabilityTheory.iIndepSet s μ<GOAL>ProbabilityTheory.iIndepFun (fun _n => m) (fun n => (s n).indicator fun _ω => 1) μ
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>One β<GOAL>1 = e.symm 1
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>Zero β<GOAL>0 = e.symm 0
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>Mul β<VAR>x y : α<GOAL>x * y = e.symm (e x * e y)
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>Add β<VAR>x y : α<GOAL>x + y = e.symm (e x + e y)
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>Div β<VAR>x y : α<GOAL>x / y = e.symm (e x / e y)
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>Sub β<VAR>x y : α<GOAL>x - y = e.symm (e x - e y)
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>Neg β<VAR>x : α<GOAL>-x = e.symm (-e x)
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>Inv β<VAR>x : α<GOAL>x⁻¹ = e.symm (e x)⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>R : Type u_1<VAR>SMul R β<VAR>r : R<VAR>x : α<GOAL>r • x = e.symm (r • e x)
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>N : Type u_1<VAR>Pow β N<VAR>n : N<VAR>x : α<GOAL>x ^ n = e.symm (e x ^ n)
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>Add β<VAR>a : α<GOAL>e.addEquiv a = e a
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>Mul β<VAR>a : α<GOAL>e.mulEquiv a = e a
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>Mul β<VAR>b : β<GOAL>(MulEquiv.symm e.mulEquiv) b = e.symm b
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>Add β<VAR>b : β<GOAL>(AddEquiv.symm e.addEquiv) b = e.symm b
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>Add β<VAR>Mul β<VAR>a : α<GOAL>e.ringEquiv a = e a
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>Add β<VAR>Mul β<VAR>b : β<GOAL>(RingEquiv.symm e.ringEquiv) b = e.symm b
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>Nontrivial β<GOAL>Nontrivial α
<VAR>α : Type u<VAR>β : Type v<VAR>Ring α<VAR>Ring β<VAR>IsDomain β<VAR>e : α ≃+* β<GOAL>IsDomain α
<VAR>α : Type u<VAR>R : Type u_1<VAR>Semiring R<VAR>Small.{v, u} α<VAR>AddCommMonoid α<VAR>Module R α<GOAL>∀ (a : α), (Shrink.linearEquiv α R).symm a = (AddEquiv.symm (equivShrink α).symm.addEquiv) a
<VAR>α : Type u<VAR>R : Type u_1<VAR>Semiring R<VAR>Small.{v, u} α<VAR>AddCommMonoid α<VAR>Module R α<GOAL>∀ (a : Shrink.{v, u} α), (Shrink.linearEquiv α R) a = (equivShrink α).symm a
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u_1<VAR>CommSemiring R<VAR>e : α ≃ β<VAR>Semiring β<VAR>Algebra R β<VAR>r : R<GOAL>let semiring := e.semiring;
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u_1<VAR>CommSemiring R<VAR>e : α ≃ β<VAR>Semiring β<VAR>Algebra R β<VAR>a : α<GOAL>(Equiv.algEquiv R e) a = e a
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u_1<VAR>CommSemiring R<VAR>e : α ≃ β<VAR>Semiring β<VAR>Algebra R β<VAR>b : β<GOAL>(AlgEquiv.symm (Equiv.algEquiv R e)) b = e.symm b
<VAR>α : Type u<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Small.{v, u} α<VAR>Semiring α<VAR>Algebra R α<GOAL>∀ (a : Shrink.{v, u} α), (Shrink.algEquiv α R) a = (equivShrink α).symm a
<VAR>α : Type u<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Small.{v, u} α<VAR>Semiring α<VAR>Algebra R α<GOAL>∀ (a : α), (Shrink.algEquiv α R).symm a = (equivShrink α) a
<VAR>G : Type u<VAR>Group G<VAR>Finite G<GOAL>∃ G' x x_1, Nonempty (G ≃* G')
<VAR>y z : ℝ<VAR>f : ℝ → ℝ≥0∞<VAR>hzy : z ≤ y<GOAL>∫⁻ (x : ℝ) in Set.Iic y, f x = (∫⁻ (x : ℝ) in Set.Iio z, f x) + ∫⁻ (x : ℝ) in Set.Icc z y, f x
<VAR>a r x : ℝ<GOAL>ProbabilityTheory.gammaPDF a r x = ENNReal.ofReal (if 0 ≤ x then r ^ a / Real.Gamma a * x ^ (a - 1) * rexp (-(r * x)) else 0)
<VAR>a r x : ℝ<VAR>hx : x < 0<GOAL>ProbabilityTheory.gammaPDF a r x = 0
<VAR>a r x : ℝ<VAR>hx : 0 ≤ x<GOAL>ProbabilityTheory.gammaPDF a r x = ENNReal.ofReal (r ^ a / Real.Gamma a * x ^ (a - 1) * rexp (-(r * x)))
<VAR>x a r : ℝ<VAR>hx : x ≤ 0<GOAL>∫⁻ (y : ℝ) in Set.Iio x, ProbabilityTheory.gammaPDF a r y = 0
<VAR>a r : ℝ<GOAL>Measurable (ProbabilityTheory.gammaPDFReal a r)
<VAR>a r : ℝ<GOAL>MeasureTheory.StronglyMeasurable (ProbabilityTheory.gammaPDFReal a r)
<VAR>x a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>hx : 0 < x<GOAL>0 < ProbabilityTheory.gammaPDFReal a r x
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>x : ℝ<GOAL>0 ≤ ProbabilityTheory.gammaPDFReal a r x
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<GOAL>∫⁻ (x : ℝ), ProbabilityTheory.gammaPDF a r x = 1
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<GOAL>MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.gammaMeasure a r)
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>x : ℝ<GOAL>↑(ProbabilityTheory.gammaCDFReal a r) x = ∫ (x : ℝ) in Set.Iic x, ProbabilityTheory.gammaPDFReal a r x
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>x : ℝ<GOAL>↑(ProbabilityTheory.gammaCDFReal a r) x = (∫⁻ (x : ℝ) in Set.Iic x, ProbabilityTheory.gammaPDF a r x).toReal
<VAR>α : Type u_1<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mΩ : MeasurableSpace Ω<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>ρCond : ProbabilityTheory.Kernel α Ω<VAR>self : ρ.IsCondKernel ρCond<GOAL>ρ.fst ⊗ₘ ρCond = ρ
<VAR>α : Type u_1<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mΩ : MeasurableSpace Ω<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>ρCond : ProbabilityTheory.Kernel α Ω<VAR>ρ.IsCondKernel ρCond<GOAL>ρ.fst ⊗ₘ ρCond = ρ
<VAR>α : Type u_1<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mΩ : MeasurableSpace Ω<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>ρCond : ProbabilityTheory.Kernel α Ω<VAR>ρ.IsCondKernel ρCond<VAR>hρ : ρ ≠ 0<GOAL>ProbabilityTheory.IsSFiniteKernel ρCond
<VAR>α : Type u_1<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mΩ : MeasurableSpace Ω<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>ρCond : ProbabilityTheory.Kernel α Ω<VAR>ρ.IsCondKernel ρCond<VAR>MeasurableSingletonClass α<VAR>x : α<VAR>hx : ρ.fst {x} ≠ 0<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>(ρCond x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)
<VAR>α : Type u_1<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mΩ : MeasurableSpace Ω<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>ρCond : ProbabilityTheory.Kernel α Ω<VAR>ρ.IsCondKernel ρCond<VAR>MeasurableSingletonClass α<VAR>x : α<VAR>hx : ρ.fst {x} ≠ 0<VAR>s : Set Ω<GOAL>(ρCond x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)
<VAR>α : Type u_1<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mΩ : MeasurableSpace Ω<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>ρCond : ProbabilityTheory.Kernel α Ω<VAR>ρ.IsCondKernel ρCond<VAR>MeasurableSingletonClass α<VAR>a : α<VAR>ha : ρ.fst {a} ≠ 0<GOAL>MeasureTheory.IsProbabilityMeasure (ρCond a)
<VAR>α : Type u_1<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mΩ : MeasurableSpace Ω<VAR>ρ : MeasureTheory.Measure (α × Ω)<VAR>MeasureTheory.IsFiniteMeasure ρ<VAR>ρCond : ProbabilityTheory.Kernel α Ω<VAR>ρ.IsCondKernel ρCond<VAR>MeasurableSingletonClass α<VAR>hρ : ∀ (a : α), ρ.fst {a} ≠ 0<GOAL>ProbabilityTheory.IsMarkovKernel ρCond
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>κCond : ProbabilityTheory.Kernel (α × β) Ω<VAR>self : κ.IsCondKernel κCond<GOAL>κ.fst ⊗ₖ κCond = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α (β × Ω)<VAR>κCond : ProbabilityTheory.Kernel (α × β) Ω<VAR>κ.IsCondKernel κCond<GOAL>κ.fst ⊗ₖ κCond = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mΩ : MeasurableSpace Ω<VAR>Countable α<VAR>κCond : α → ProbabilityTheory.Kernel β Ω<VAR>h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y<VAR>p : α × β<GOAL>(ProbabilityTheory.Kernel.condKernelCountable κCond h_atom) p = (κCond p.1) p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>f : α → γ<VAR>g : β → γ<VAR>μ : autoParam (MeasureTheory.Measure α) _auto✝<VAR>ν : autoParam (MeasureTheory.Measure β) _auto✝¹<VAR>self : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>MeasureTheory.Measure.map f μ = MeasureTheory.Measure.map g ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>f : α → γ<VAR>g : β → γ<VAR>μ : autoParam (MeasureTheory.Measure α) _auto✝<VAR>ν : autoParam (MeasureTheory.Measure β) _auto✝¹<VAR>self : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>f : α → γ<VAR>g : β → γ<VAR>μ : autoParam (MeasureTheory.Measure α) _auto✝<VAR>ν : autoParam (MeasureTheory.Measure β) _auto✝¹<VAR>self : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>AEMeasurable g ν
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace γ<VAR>μ : MeasureTheory.Measure α<VAR>f : α → γ<VAR>hf : AEMeasurable f μ<GOAL>ProbabilityTheory.IdentDistrib f f μ μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>ProbabilityTheory.IdentDistrib g f ν μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>MeasurableSpace δ<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>ρ : MeasureTheory.Measure δ<VAR>h : δ → γ<VAR>h₁ : ProbabilityTheory.IdentDistrib f g μ ν<VAR>h₂ : ProbabilityTheory.IdentDistrib g h ν ρ<GOAL>ProbabilityTheory.IdentDistrib f h μ ρ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>MeasurableSpace δ<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>u : γ → δ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<VAR>hu : AEMeasurable u (MeasureTheory.Measure.map f μ)<GOAL>ProbabilityTheory.IdentDistrib (u ∘ f) (u ∘ g) μ ν