mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
μ : Measure 𝓧
inst✝¹ : SFinite μ
π : Measure Θ
inst✝ : SFinite π
hl_pos : μ Set.univ = ∞ → ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂π = 0 → ∃ y, ∫⁻ (θ : Θ), ℓ θ y ∂π = 0
h_zero : μ = 0 → Nonempty 𝓨
⊢ bayesRisk ℓ (Kernel.const Θ μ) π = ⨅ y, ∫⁻ (θ : Θ), ℓ θ y * μ Set.univ ∂π

Tactic:
refine le_antisymm ((bayesRisk_le_iInf' hl _ _).trans_eq (by simp)) ?_
  simp_rw [bayesRisk, le_iInf_iff]
  intro κ hκ
  rw [avgRisk_const_left' hl]
  refine le_trans ?_ (iInf_mul_le_lintegral (fun y ↦ ∫⁻ θ, ℓ θ y ∂π))
  rw [Measure.comp_apply_univ, ENNReal.iInf_mul' hl_pos (fun hμ ↦ h_zero (by simpa using hμ))]
  gcongr with y
  rw [lintegral_mul_const]
  fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case mt
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X i.fst i.snd)
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
⊢ ∀ (i : ι) (x : κ i), ⟨i, x⟩ ∈ s → MeasurableSet ((↑(s.preimage (Sigma.mk i) ⋯)).pi fun j ↦ t ⟨i, j⟩)

Tactic:
exact fun i j hij ↦ MeasurableSet.pi (countable_toSet _) fun k hk ↦ by simp_all

Goal state after:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝² : Subsingleton 𝓧
inst✝¹ : Nonempty 𝓨
inst✝ : SFinite π
hl : Measurable (uncurry ℓ)
⊢ bayesRisk ℓ P π = ⨅ y, ∫⁻ (θ : Θ), ℓ θ y * (P θ) Set.univ ∂π

Tactic:
refine le_antisymm (bayesRisk_le_iInf' hl _ _) ?_
  rw [bayesRisk_eq_iInf_measure_of_subsingleton]
  simp only [avgRisk_const_right', le_iInf_iff]
  refine fun μ hμ ↦ (iInf_le_lintegral (μ := μ) _).trans_eq ?_
  rw [lintegral_lintegral_swap]
  · congr with θ
    rw [lintegral_mul_const _ (by fun_prop), mul_comm]
  · have := P.measurable_coe .univ
    fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: 𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
π : Measure Bool
inst✝ : IsFiniteMeasure π
⊢ ∀ᵐ (x : 𝓧) ∂⇑(Kernel.boolKernel μ ν) ∘ₘ π,
    (((Kernel.boolKernel μ ν)†π) x) {false} = π {false} * (∂μ/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x

Tactic:
filter_upwards [posterior_eq_withDensity_of_countable (Kernel.boolKernel μ ν) π] with x hx
  rw [hx]
  simp

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: 𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
π : Measure Bool
inst✝ : IsFiniteMeasure π
⊢ ∀ᵐ (x : 𝓧) ∂⇑(Kernel.boolKernel μ ν) ∘ₘ π,
    (((Kernel.boolKernel μ ν)†π) x) {true} = π {true} * (∂ν/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x

Tactic:
filter_upwards [posterior_eq_withDensity_of_countable (Kernel.boolKernel μ ν) π] with x hx
  rw [hx]
  simp

Goal state after:
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: p : ↑I
⊢ Bin(0, p) = dirac 0

Tactic:
by simp [binomial]

Goal state after:
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
⊢ ∫⁻ (x : ℝ) in Iic y, f x = (∫⁻ (x : ℝ) in Iio z, f x) + ∫⁻ (x : ℝ) in Icc z y, f x

Tactic:
← Iio_union_Icc_eq_Iic hzy,

Goal state after:
y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
⊢ ∫⁻ (x : ℝ) in Iio z ∪ Icc z y, f x = (∫⁻ (x : ℝ) in Iio z, f x) + ∫⁻ (x : ℝ) in Icc z y, f x
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : PMF α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : s ∩ p.support = t ∩ p.support
⊢ p.toMeasure s = p.toMeasure t

Tactic:
by
  simpa only [p.toMeasure_apply_eq_toOuterMeasure_apply, hs, ht] using
    p.toOuterMeasure_apply_eq_of_inter_support_eq h

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
p : PMF α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ p.toMeasure = μ ↔ p = μ.toPMF

Tactic:
rw [← toMeasure_inj, Measure.toPMF_toMeasure]

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
p : PMF α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ μ.toPMF = p ↔ μ = p.toMeasure

Tactic:
rw [← toMeasure_inj, Measure.toPMF_toMeasure]

Goal state after:
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ (∫⁻ (a_1 : ℝ) in Iic x, gammaPDF a r a_1).toReal = ∫ (x : ℝ) in Iic x, gammaPDFReal a r x

Tactic:
refine (integral_eq_lintegral_of_nonneg_ae ?_ ?_).symm

Goal state after:
case refine_1
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ 0 ≤ᵐ[volume.restrict (Iic x)] gammaPDFReal a r

case refine_2
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ AEStronglyMeasurable (gammaPDFReal a r) (volume.restrict (Iic x))
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫ (a : ℝ) in Icc 0 x, r * rexp (-(r * a)) ∂volume = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal

Tactic:
have : ∫ a in uIoc 0 x, r * rexp (-(r * a)) = ∫ a in 0..x, r * rexp (-(r * a)) := by
        rw [intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_eq_mul, if_pos h, one_mul]
      rw [integral_Icc_eq_integral_Ioc, ← uIoc_of_le h, this]
      rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h
        (f := fun a ↦ -1 * rexp (-(r * a))) _ _]
      · rw [ENNReal.toReal_ofReal_eq_iff.2
          (sub_nonneg.2 (Real.exp_le_one_iff.2 <| by nlinarith))]
        norm_num; ring
      · simp only [intervalIntegrable_iff, uIoc_of_le h]
        exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
      · have : Continuous (fun a ↦ rexp (-(r * a))) := by
          simp only [← neg_mul]; exact (continuous_const_mul (-r)).rexp
        exact Continuous.continuousOn (Continuous.comp' (continuous_const_mul (-1)) this)
      · simp only [neg_mul, one_mul]
        exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝⁴ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝³ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_cf : Integrable ((traj κ a) x₀)[f | ↑piLE c] ((traj κ a) x₀)
mcf : StronglyMeasurable ((traj κ a) x₀)[f | ↑piLE c]
x : (n : ℕ) → X n
h1 : ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x = ((traj κ a) x₀)[f | ↑piLE b] x
⊢ ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x =
      ∫ (y : (n : ℕ) → X n), ((traj κ a) x₀)[f | ↑piLE c] y ∂(traj κ b) (frestrictLe b x) →
    ((traj κ a) x₀)[f | ↑piLE b] x =
      ∫ (y : (i : ↥(Iic c)) → X ↑i),
        ((traj κ a) x₀)[f | ↑piLE c] (updateFinset x (Iic c) y) ∂(partialTraj κ b c) (frestrictLe b x)

Tactic:
h2

Goal state after:
X : ℕ → Type u_1
inst✝⁴ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝³ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_cf : Integrable ((traj κ a) x₀)[f | ↑piLE c] ((traj κ a) x₀)
mcf : StronglyMeasurable ((traj κ a) x₀)[f | ↑piLE c]
x : (n : ℕ) → X n
h1 : ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x = ((traj κ a) x₀)[f | ↑piLE b] x
h2 :
  ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x =
    ∫ (y : (n : ℕ) → X n), ((traj κ a) x₀)[f | ↑piLE c] y ∂(traj κ b) (frestrictLe b x)
⊢ ((traj κ a) x₀)[f | ↑piLE b] x =
    ∫ (y : (i : ↥(Iic c)) → X ↑i),
      ((traj κ a) x₀)[f | ↑piLE c] (updateFinset x (Iic c) y) ∂(partialTraj κ b c) (frestrictLe b x)
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ (∫⁻ (a : ℝ) in Iic x, paretoPDF t r a).toReal = ∫ (x : ℝ) in Iic x, paretoPDFReal t r x

Tactic:
refine (integral_eq_lintegral_of_nonneg_ae ?_ ?_).symm

Goal state after:
case refine_1
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ 0 ≤ᵐ[volume.restrict (Iic x)] paretoPDFReal t r

case refine_2
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ AEStronglyMeasurable (paretoPDFReal t r) (volume.restrict (Iic x))
Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm

Goal state before:
pp: p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun n ↦ ↑n * p n) atTop (𝓝 r)
⊢ (fun n ↦ ↑n ^ k / ↑k.factorial * p n ^ k) = fun n ↦ (↑n * p n) ^ k / ↑k.factorial

Tactic:
by ext; field

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
H : ¬(f a' h) b = 0
⊢ p a' * (f a' h) b * 0 = p a' * ((f a' h) b * (g b ⋯) a)

Tactic:
absurd H
    simpa [h] using h_1 a'

Goal state after:
Module: Mathlib.Probability.Kernel.Category.Stoch

Goal state before:
pp: X Y : Stoch
κ : X ⟶ Y
⊢ ε ≫ Δ = Δ ≫ (ε ⊗ₘ ε)

Tactic:
ext : 1
    simp only [WideSubcategory.comp_def, MorphismProperty.counit_hom]
    cat_disch

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : ι → Type u_3
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
hf : ∀ (i : ι), Measurable (f i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndep m' hm' (fun x ↦ MeasurableSpace.comap (f x) (m x)) μ ↔
    ∀ (s : Finset ι) {g : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (g i)) →
        μ[(⋂ i ∈ s, g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(g i).indicator fun ω ↦ 1 | m']

Tactic:
rw [iCondIndep_iff]

Goal state after:
case hm
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : ι → Type u_3
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
hf : ∀ (i : ι), Measurable (f i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ (i : ι), MeasurableSpace.comap (f i) (m i) ≤ mΩ
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
κ : Kernel X.carrier Y.carrier
inst✝¹ : IsDeterministic κ
inst✝ : IsMarkovKernel κ
⊢ { hom := κ, property := ⋯ } ≫ Δ = Δ ≫ ({ hom := κ, property := ⋯ } ⊗ₘ { hom := κ, property := ⋯ })

Tactic:
by
    ext : 1; dsimp
    rw [Kernel.id_parallelComp_comp_parallelComp_id]
    exact (Kernel.parallelComp_self_comp_copy).symm

Goal state after:
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
inst✝ : SigmaFinite (μ.trim ⋯)
hin : i ≤ n
⊢ μ[f n | hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = ↑i}] f i

Tactic:
by
  refine Filter.EventuallyEq.trans ?_ (ae_restrict_of_ae (h.condExp_ae_eq hin))
  refine condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le (ℱ.le i)
    (hτ.measurableSet_eq' i) fun t => ?_
  rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]

Goal state after:
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
h2 : ∀ (ω : Ω), f (A.indicator 1 ω) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω
hg : ∀ {c : ℝ}, Integrable (fun ω ↦ c * ∏ s, (g s) (X s ω)) P
⊢ ∫ (x : Ω),
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) x + f 0 * ∏ x_1, (g x_1) (X x_1 x) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) x ∂P =
    (∫ (x : Ω), f (A.indicator 1 x) ∂P) * ∫ (x : Ω), ∏ x_1, (g x_1) (X x_1 x) ∂P

Tactic:
h2

Goal state after:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
h2 : ∀ (ω : Ω), f (A.indicator 1 ω) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω
hg : ∀ {c : ℝ}, Integrable (fun ω ↦ c * ∏ s, (g s) (X s ω)) P
⊢ ∫ (x : Ω),
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) x + f 0 * ∏ x_1, (g x_1) (X x_1 x) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) x ∂P =
    (∫ (x : Ω), A.indicator (fun x ↦ f 1) x + Aᶜ.indicator (fun x ↦ f 0) x ∂P) * ∫ (x : Ω), ∏ x_1, (g x_1) (X x_1 x) ∂P
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ (μ.tilted fun x ↦ t * X x) s = ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)

Tactic:
simp_rw [tilted_mul_apply_eq_ofReal_integral_mgf' hs, exp_sub]
    rwa [exp_cgf]

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
h1_symm : Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map (⇑e.symm) (Measure.map (fun x ↦ ((k x, g x), f x)) μ)
h2 :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
h2_symm :
  ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ =
    Measure.map (⇑e.symm) (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ)
⊢ Measure.map (fun ω ↦ (k ω, g ω, f ω)) μ =
      ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ ↔
    Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ) =
      ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ

Tactic:
h2

Goal state after:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
h1_symm : Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map (⇑e.symm) (Measure.map (fun x ↦ ((k x, g x), f x)) μ)
h2 :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
h2_symm :
  ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ =
    Measure.map (⇑e.symm) (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ)
⊢ Measure.map (fun ω ↦ (k ω, g ω, f ω)) μ =
      ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ ↔
    Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ) =
      Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
⊢ log (rexp (↑c * t ^ 2 / 2)) ≤ ↑c * t ^ 2 / 2

Tactic:
by rw [log_exp]

Goal state after:
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

Tactic:
by
  suffices (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0 by
    filter_upwards [this] with ω hω
    simpa [hX.p_pos, not_lt_of_gt hX.p_pos] using hω
  rw [← lintegral_eq_zero_iff' (hX.aemeasurable_edist.pow_const p), ← nonpos_iff_eq_zero]
  calc ∫⁻ ω, edist (X s ω) (X t ω) ^ p ∂P
  _ ≤ 0 * edist s t ^ q := hX.kolmogorovCondition s t
  _ = 0 := by simp

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
ω' : Ω'
h1 : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
⊢ (∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')) →
    IsFiniteMeasure (κ ω') → ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-t * ε + ↑c * t ^ 2 / 2)

Tactic:
h2

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
ω' : Ω'
h1 : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h2 : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
⊢ IsFiniteMeasure (κ ω') → ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-t * ε + ↑c * t ^ 2 / 2)
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p q : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
x✝ : Locally p 𝓕 X P ∧ Locally q 𝓕 X P
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
n : ℕ
this :
  ∀ (p q : (ι → Ω → E) → Prop),
    IsStable 𝓕 p →
      IsStable 𝓕 q →
        ∀ (hpX : Locally p 𝓕 X P) (hqX : Locally q 𝓕 X P),
          p
            (stoppedProcess (fun i ↦ {ω | ⊥ < (hpX.localSeq ⊓ hqX.localSeq) n ω}.indicator (X i))
              ((hpX.localSeq ⊓ hqX.localSeq) n))
⊢ (fun Y ↦ p Y ∧ q Y)
    (stoppedProcess (fun i ↦ {ω | ⊥ < (hpX.localSeq ⊓ hqX.localSeq) n ω}.indicator (X i))
      ((hpX.localSeq ⊓ hqX.localSeq) n))

Tactic:
refine ⟨this p q hp hq hpX hqX, ?_⟩

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p q : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
x✝ : Locally p 𝓕 X P ∧ Locally q 𝓕 X P
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
n : ℕ
this :
  ∀ (p q : (ι → Ω → E) → Prop),
    IsStable 𝓕 p →
      IsStable 𝓕 q →
        ∀ (hpX : Locally p 𝓕 X P) (hqX : Locally q 𝓕 X P),
          p
            (stoppedProcess (fun i ↦ {ω | ⊥ < (hpX.localSeq ⊓ hqX.localSeq) n ω}.indicator (X i))
              ((hpX.localSeq ⊓ hqX.localSeq) n))
⊢ q
    (stoppedProcess (fun i ↦ {ω | ⊥ < (hpX.localSeq ⊓ hqX.localSeq) n ω}.indicator (X i))
      ((hpX.localSeq ⊓ hqX.localSeq) n))
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω' : Ω'
h1 : (κ ω') {ω | 0 < (-X) ω} = 0
⊢ (κ ω') {ω | 0 < X ω} = 0 → X =ᵐ[κ ω'] 0

Tactic:
h2

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω' : Ω'
h1 : (κ ω') {ω | 0 < (-X) ω} = 0
h2 : (κ ω') {ω | 0 < X ω} = 0
⊢ X =ᵐ[κ ω'] 0
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cX
q : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cY
ω' : Ω'
⊢ (∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑cX * t ^ 2 / 2)) →
    (∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑cY * t ^ 2 / 2)) →
      (∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')) →
        (∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * Y ω)) (↑q) (κ ω')) →
          ∀ (t : ℝ), mgf (fun ω ↦ X ω + Y ω) (κ ω') t ≤ rexp (↑((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) * t ^ 2 / 2)

Tactic:
hmX

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cX
q : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cY
ω' : Ω'
hmX : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑cX * t ^ 2 / 2)
⊢ (∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑cY * t ^ 2 / 2)) →
    (∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')) →
      (∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * Y ω)) (↑q) (κ ω')) →
        ∀ (t : ℝ), mgf (fun ω ↦ X ω + Y ω) (κ ω') t ≤ rexp (↑((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) * t ^ 2 / 2)