ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 : Measurable u<GOAL>ProbabilityTheory.IdentDistrib (u ∘ f) (u ∘ g) μ ν
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace γ<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → γ<VAR>hf : AEMeasurable f μ<VAR>heq : f =ᵐ[μ] g<GOAL>ProbabilityTheory.IdentDistrib f 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 (AEMeasurable.mk f hf) μ μ
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace γ<VAR>μ : MeasureTheory.Measure α<VAR>f : α → γ<VAR>TopologicalSpace γ<VAR>TopologicalSpace.PseudoMetrizableSpace γ<VAR>BorelSpace γ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>ProbabilityTheory.IdentDistrib f (MeasureTheory.AEStronglyMeasurable.mk f hf) μ μ
<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 μ ν<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>μ (f ⁻¹' s) = ν (g ⁻¹' s)
<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 μ ν<VAR>p : γ → Prop<VAR>pmeas : MeasurableSet {x | p x}<VAR>hp : ∀ᵐ (x : α) ∂μ, p (f x)<GOAL>∀ᵐ (x : β) ∂ν, p (g x)
<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 μ ν<VAR>t : Set γ<VAR>tmeas : MeasurableSet t<VAR>ht : ∀ᵐ (x : α) ∂μ, f x ∈ t<GOAL>∀ᵐ (x : β) ∂ν, g x ∈ t
<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>TopologicalSpace γ<VAR>TopologicalSpace.MetrizableSpace γ<VAR>OpensMeasurableSpace γ<VAR>SecondCountableTopology γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>MeasureTheory.AEStronglyMeasurable 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>TopologicalSpace γ<VAR>TopologicalSpace.MetrizableSpace γ<VAR>BorelSpace γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable g ν
<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>TopologicalSpace γ<VAR>TopologicalSpace.MetrizableSpace γ<VAR>BorelSpace γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>MeasureTheory.AEStronglyMeasurable f μ ↔ MeasureTheory.AEStronglyMeasurable g ν
<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>ConditionallyCompleteLinearOrder γ<VAR>TopologicalSpace γ<VAR>OpensMeasurableSpace γ<VAR>OrderClosedTopology γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>essSup f μ = essSup g ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>f : α → ℝ≥0∞<VAR>g : β → ℝ≥0∞<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>∫⁻ (x : α), f x ∂μ = ∫⁻ (x : β), g x ∂ν
<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>NormedAddCommGroup γ<VAR>NormedSpace ℝ γ<VAR>BorelSpace γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>∫ (x : α), f x ∂μ = ∫ (x : β), g x ∂ν
<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>NormedAddCommGroup γ<VAR>OpensMeasurableSpace γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<VAR>p : ℝ≥0∞<GOAL>MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p ν
<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>NormedAddCommGroup γ<VAR>BorelSpace γ<VAR>p : ℝ≥0∞<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp g p ν
<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>NormedAddCommGroup γ<VAR>BorelSpace γ<VAR>p : ℝ≥0∞<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>MeasureTheory.Memℒp f p μ ↔ MeasureTheory.Memℒp g p ν
<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>NormedAddCommGroup γ<VAR>BorelSpace γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable g ν
<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>NormedAddCommGroup γ<VAR>BorelSpace γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>MeasureTheory.Integrable f μ ↔ MeasureTheory.Integrable g ν
<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>NormedAddCommGroup γ<VAR>BorelSpace γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>ProbabilityTheory.IdentDistrib (fun x => ‖f x‖) (fun x => ‖g x‖) μ ν
<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>NormedAddCommGroup γ<VAR>BorelSpace γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>ProbabilityTheory.IdentDistrib (fun x => ‖f x‖₊) (fun x => ‖g x‖₊) μ ν
<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>Pow γ ℕ<VAR>MeasurablePow γ ℕ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<VAR>n : ℕ<GOAL>ProbabilityTheory.IdentDistrib (fun x => f x ^ n) (fun x => g x ^ n) μ ν
<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>Pow γ ℕ<VAR>MeasurablePow γ ℕ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>ProbabilityTheory.IdentDistrib (fun x => f x ^ 2) (fun x => g x ^ 2) μ ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>f : α → ℝ≥0<VAR>g : β → ℝ≥0<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>ProbabilityTheory.IdentDistrib (fun x => ↑(f x)) (fun x => ↑(g x)) μ ν
<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>Add γ<VAR>MeasurableAdd γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<VAR>c : γ<GOAL>ProbabilityTheory.IdentDistrib (fun x => f x + c) (fun x => g x + c) μ ν
<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>Mul γ<VAR>MeasurableMul γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<VAR>c : γ<GOAL>ProbabilityTheory.IdentDistrib (fun x => f x * c) (fun x => g x * c) μ ν
<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>Add γ<VAR>MeasurableAdd γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<VAR>c : γ<GOAL>ProbabilityTheory.IdentDistrib (fun x => c + f x) (fun x => c + g x) μ ν
<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>Mul γ<VAR>MeasurableMul γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<VAR>c : γ<GOAL>ProbabilityTheory.IdentDistrib (fun x => c * f x) (fun x => c * g x) μ ν
<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>Div γ<VAR>MeasurableDiv γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<VAR>c : γ<GOAL>ProbabilityTheory.IdentDistrib (fun x => f x / c) (fun x => g x / c) μ ν
<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>Sub γ<VAR>MeasurableSub γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<VAR>c : γ<GOAL>ProbabilityTheory.IdentDistrib (fun x => f x - c) (fun x => g x - c) μ ν
<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>Div γ<VAR>MeasurableDiv γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<VAR>c : γ<GOAL>ProbabilityTheory.IdentDistrib (fun x => c / f x) (fun x => c / g x) μ ν
<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>Sub γ<VAR>MeasurableSub γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<VAR>c : γ<GOAL>ProbabilityTheory.IdentDistrib (fun x => c - f x) (fun x => c - g x) μ ν
<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>Inv γ<VAR>MeasurableInv γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>ProbabilityTheory.IdentDistrib f⁻¹ g⁻¹ μ ν
<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>Neg γ<VAR>MeasurableNeg γ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>ProbabilityTheory.IdentDistrib (-f) (-g) μ ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>f : α → ℝ<VAR>g : β → ℝ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>ProbabilityTheory.evariance f μ = ProbabilityTheory.evariance g ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>f : α → ℝ<VAR>g : β → ℝ<VAR>h : ProbabilityTheory.IdentDistrib f g μ ν<GOAL>ProbabilityTheory.variance f μ = ProbabilityTheory.variance g ν
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>E : Type u_5<VAR>MeasurableSpace E<VAR>NormedAddCommGroup E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : MeasureTheory.Memℒp (f j) p μ<VAR>hfmeas : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)<VAR>hf : ∀ (i : ι), ProbabilityTheory.IdentDistrib (f i) (f j) μ μ<GOAL>MeasureTheory.UniformIntegrable f p μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>E : Type u_5<VAR>MeasurableSpace E<VAR>NormedAddCommGroup E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : MeasureTheory.Memℒp (f j) p μ<VAR>hf : ∀ (i : ι), ProbabilityTheory.IdentDistrib (f i) (f j) μ μ<GOAL>MeasureTheory.UniformIntegrable f p μ
<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>MeasureTheory.IsFiniteMeasure μ<VAR>MeasureTheory.IsFiniteMeasure μ'<VAR>X : γ → α<VAR>X' : δ → α<VAR>Y : γ → β<VAR>Y' : δ → β<VAR>h_indep : ProbabilityTheory.IndepFun X Y μ<VAR>h_ident : ProbabilityTheory.IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'<GOAL>ProbabilityTheory.IndepFun X' Y' μ'
<VAR>r x : ℝ<GOAL>ProbabilityTheory.exponentialPDF r x = ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0)
<VAR>r x : ℝ<VAR>hx : x < 0<GOAL>ProbabilityTheory.exponentialPDF r x = 0
<VAR>r x : ℝ<VAR>hx : 0 ≤ x<GOAL>ProbabilityTheory.exponentialPDF r x = ENNReal.ofReal (r * rexp (-(r * x)))
<VAR>x r : ℝ<VAR>hx : x ≤ 0<GOAL>∫⁻ (y : ℝ) in Set.Iio x, ProbabilityTheory.exponentialPDF r y = 0
<VAR>r : ℝ<GOAL>Measurable (ProbabilityTheory.exponentialPDFReal r)
<VAR>r : ℝ<GOAL>MeasureTheory.StronglyMeasurable (ProbabilityTheory.exponentialPDFReal r)
<VAR>x r : ℝ<VAR>hr : 0 < r<VAR>hx : 0 < x<GOAL>0 < ProbabilityTheory.exponentialPDFReal r x
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : ℝ<GOAL>0 ≤ ProbabilityTheory.exponentialPDFReal r x
<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>∫⁻ (x : ℝ), ProbabilityTheory.exponentialPDF r x = 1
<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.expMeasure r)
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : ℝ<GOAL>↑(ProbabilityTheory.exponentialCDFReal r) x = ∫ (x : ℝ) in Set.Iic x, ProbabilityTheory.exponentialPDFReal r x
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : ℝ<GOAL>↑(ProbabilityTheory.exponentialCDFReal r) x = (∫⁻ (x : ℝ) in Set.Iic x, ProbabilityTheory.exponentialPDF r x).toReal
<VAR>b x : ℝ<VAR>hb : 0 < b<GOAL>MeasureTheory.IntegrableOn (fun x => rexp (-(b * x))) (Set.Ioc 0 x) MeasureTheory.volume
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : ℝ<GOAL>∫⁻ (y : ℝ) in Set.Iic x, ProbabilityTheory.exponentialPDF r y = ENNReal.ofReal (if 0 ≤ x then 1 - rexp (-(r * x)) else 0)
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : ℝ<GOAL>↑(ProbabilityTheory.exponentialCDFReal r) x = if 0 ≤ x then 1 - rexp (-(r * x)) else 0
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>X : Ω → E<VAR>ℙ : MeasureTheory.Measure Ω<VAR>μ : autoParam (MeasureTheory.Measure E) _auto✝<VAR>self : MeasureTheory.HasPDF X ℙ μ<GOAL>AEMeasurable X ℙ ∧ (MeasureTheory.Measure.map X ℙ).HaveLebesgueDecomposition μ ∧ MeasureTheory.Measure.map X ℙ ≪ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<GOAL>∀ {x : MeasurableSpace Ω} {X : Ω → E} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E}, MeasureTheory.HasPDF X ℙ μ ↔ AEMeasurable X ℙ ∧ (MeasureTheory.Measure.map X ℙ).HaveLebesgueDecomposition μ ∧ MeasureTheory.Measure.map X ℙ ≪ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<GOAL>∀ {x : MeasurableSpace Ω} {X : Ω → E} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E}, AEMeasurable X ℙ → (MeasureTheory.HasPDF X ℙ μ ↔ (MeasureTheory.Measure.map X ℙ).HaveLebesgueDecomposition μ ∧ MeasureTheory.Measure.map X ℙ ≪ μ)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<GOAL>∀ {x : MeasurableSpace Ω} (X : Ω → E) (ℙ : MeasureTheory.Measure Ω) (μ : MeasureTheory.Measure E) [hX : MeasureTheory.HasPDF X ℙ μ], AEMeasurable X ℙ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<GOAL>∀ {x : MeasurableSpace Ω} {X : Ω → E} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} [hX : MeasureTheory.HasPDF X ℙ μ], MeasureTheory.Measure.map X ℙ ≪ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<GOAL>∀ {x : MeasurableSpace Ω} (X : Ω → E) (ℙ : MeasureTheory.Measure Ω) (μ : MeasureTheory.Measure E) [inst : MeasureTheory.HasPDF X ℙ μ], Measurable X → MeasureTheory.Measure.QuasiMeasurePreserving X ℙ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<GOAL>∀ {x : MeasurableSpace Ω} {X Y : Ω → E} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E}, X =ᵐ[ℙ] Y → ∀ [hX : MeasureTheory.HasPDF X ℙ μ], MeasureTheory.HasPDF Y ℙ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<GOAL>∀ {x : MeasurableSpace Ω} {X Y : Ω → E} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E}, X =ᵐ[ℙ] Y → (MeasureTheory.HasPDF X ℙ μ ↔ MeasureTheory.HasPDF Y ℙ μ)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<GOAL>∀ {x : MeasurableSpace Ω} {X : Ω → E} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E}, AEMeasurable X ℙ → ∀ (f : E → ℝ≥0∞), AEMeasurable f μ → MeasureTheory.Measure.map X ℙ = μ.withDensity f → MeasureTheory.HasPDF X ℙ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<GOAL>∀ {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} {X : Ω → E}, MeasureTheory.pdf X ℙ μ = (MeasureTheory.Measure.map X ℙ).rnDeriv μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<GOAL>∀ {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} {X : Ω → E}, ¬AEMeasurable X ℙ → MeasureTheory.pdf X ℙ μ =ᵐ[μ] 0
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<GOAL>∀ {x : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} {X : Ω → E}, ¬(MeasureTheory.Measure.map X ℙ).HaveLebesgueDecomposition μ → MeasureTheory.pdf X ℙ μ = 0
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : MeasureTheory.Measure Ω<VAR>μ : MeasureTheory.Measure E<VAR>X : Ω → E<VAR>h : ¬MeasureTheory.pdf X ℙ μ =ᵐ[μ] 0<GOAL>AEMeasurable X ℙ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : MeasureTheory.Measure Ω<VAR>μ : MeasureTheory.Measure E<VAR>X : Ω → E<VAR>hac : MeasureTheory.Measure.map X ℙ ≪ μ<VAR>hpdf : ¬MeasureTheory.pdf X ℙ μ =ᵐ[μ] 0<GOAL>MeasureTheory.HasPDF X ℙ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>X : Ω → E<VAR>ℙ : MeasureTheory.Measure Ω<VAR>μ : MeasureTheory.Measure E := by volume_tac<GOAL>Measurable (MeasureTheory.pdf X ℙ μ)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<GOAL>∀ {x : MeasurableSpace Ω} (X : Ω → E) (ℙ : MeasureTheory.Measure Ω) (μ : autoParam (MeasureTheory.Measure E) _auto✝), MeasureTheory.Measure.withDensity μ (MeasureTheory.pdf X ℙ μ) ≤ MeasureTheory.Measure.map X ℙ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>X : Ω → E<VAR>ℙ : MeasureTheory.Measure Ω<VAR>μ : MeasureTheory.Measure E := by volume_tac<VAR>s : Set E<GOAL>∫⁻ (x : E) in s, MeasureTheory.pdf X ℙ μ x ∂μ ≤ (MeasureTheory.Measure.map X ℙ) s
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>X : Ω → E<VAR>ℙ : MeasureTheory.Measure Ω<VAR>μ : MeasureTheory.Measure E := by volume_tac<VAR>hX : MeasureTheory.HasPDF X ℙ μ<GOAL>MeasureTheory.Measure.map X ℙ = MeasureTheory.Measure.withDensity μ (MeasureTheory.pdf X ℙ μ)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>X : Ω → E<VAR>ℙ : MeasureTheory.Measure Ω<VAR>μ : MeasureTheory.Measure E := by volume_tac<VAR>hX : MeasureTheory.HasPDF X ℙ μ<VAR>s : Set E<VAR>hs : MeasurableSet s<GOAL>(MeasureTheory.Measure.map X ℙ) s = ∫⁻ (x : E) in s, MeasureTheory.pdf X ℙ μ x ∂μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : MeasureTheory.Measure Ω<VAR>μ : MeasureTheory.Measure E<VAR>X Y : Ω → E<VAR>hXY : X =ᵐ[ℙ] Y<GOAL>MeasureTheory.pdf X ℙ μ = MeasureTheory.pdf Y ℙ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : MeasureTheory.Measure Ω<VAR>μ : MeasureTheory.Measure E<VAR>X : Ω → E<VAR>MeasureTheory.HasPDF X ℙ μ<GOAL>∫⁻ (x : E), MeasureTheory.pdf X ℙ μ x ∂μ = ℙ Set.univ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : MeasureTheory.Measure Ω<VAR>μ : MeasureTheory.Measure E<VAR>MeasureTheory.IsFiniteMeasure ℙ<VAR>X : Ω → E<VAR>MeasureTheory.HasPDF X ℙ μ<VAR>f : E → ℝ≥0∞<VAR>hmf : AEMeasurable f μ<GOAL>MeasureTheory.Measure.map X ℙ = μ.withDensity f ↔ MeasureTheory.pdf X ℙ μ =ᵐ[μ] f
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : MeasureTheory.Measure Ω<VAR>μ : MeasureTheory.Measure E<VAR>MeasureTheory.SigmaFinite μ<VAR>X : Ω → E<VAR>MeasureTheory.HasPDF X ℙ μ<VAR>f : E → ℝ≥0∞<VAR>hmf : AEMeasurable f μ<GOAL>MeasureTheory.Measure.map X ℙ = μ.withDensity f ↔ MeasureTheory.pdf X ℙ μ =ᵐ[μ] f
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure ℙ<VAR>μ : MeasureTheory.Measure E<VAR>X : Ω → E<GOAL>∀ᵐ (x : E) ∂μ, MeasureTheory.pdf X ℙ μ x < ⊤
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : MeasureTheory.Measure Ω<VAR>μ : MeasureTheory.Measure E<VAR>MeasureTheory.IsFiniteMeasure ℙ<VAR>X : Ω → E<GOAL>(fun x => ENNReal.ofReal (MeasureTheory.pdf X ℙ μ x).toReal) =ᵐ[μ] MeasureTheory.pdf X ℙ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : MeasureTheory.Measure Ω<VAR>μ : MeasureTheory.Measure E<VAR>X : Ω → E<VAR>MeasureTheory.HasPDF X ℙ μ<VAR>f : E → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>∫⁻ (x : E), MeasureTheory.pdf X ℙ μ x * f x ∂μ = ∫⁻ (x : Ω), f (X x) ∂ℙ
<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>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>MeasureTheory.IsFiniteMeasure ℙ<VAR>X : Ω → E<VAR>MeasureTheory.HasPDF X ℙ μ<VAR>f : E → F<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.Integrable (fun x => (MeasureTheory.pdf X ℙ μ x).toReal • f x) μ ↔ MeasureTheory.Integrable (fun x => f (X x)) ℙ
<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>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>MeasureTheory.IsFiniteMeasure ℙ<VAR>X : Ω → E<VAR>MeasureTheory.HasPDF X ℙ μ<VAR>f : E → F<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>∫ (x : E), (MeasureTheory.pdf X ℙ μ x).toReal • f x ∂μ = ∫ (x : Ω), f (X x) ∂ℙ
<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>MeasureTheory.HasPDF X ℙ μ<VAR>hX : AEMeasurable X ℙ<VAR>g : E → F<VAR>hg : MeasureTheory.Measure.QuasiMeasurePreserving g μ ν<VAR>hmap : (MeasureTheory.Measure.map g (MeasureTheory.Measure.map X ℙ)).HaveLebesgueDecomposition ν<GOAL>MeasureTheory.HasPDF (g ∘ X) ℙ ν