Theorems · Theorem · probability

ProbabilityTheory.IndepFun.exp_mul

∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ},
  ProbabilityTheory.IndepFun X Y μ →
    ∀ (s t : ℝ), ProbabilityTheory.IndepFun (fun ω => Real.exp (s * X ω)) (fun ω => Real.exp (t * Y ω)) μ

This is a trivial application of IndepFun.comp but it will come up frequently.

Defined in

Mathlib.Probability.Moments.Basic

Cited by

2 results in Mathlib

Foundations

Depth 181 from the axioms · uses propext, Classical.choice, Quot.sound