mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ MeasurableSet {a | (κ.singularPart η) a = 0}

Tactic:
singularPart_eq_zero_iff_measure_eq_zero

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ MeasurableSet {a | (κ a) (κ.mutuallySingularSetSlice η a) = 0}
Module: Mathlib.Probability.Kernel.CompProdEqIff

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝³ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ_eq : ∀ᵐ (a : α) ∂μ, κ a = (η.withDensity (κ.rnDeriv η)) a
this : ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂η a, κ.rnDeriv η a b = 1
a : α
⊢ κ a ≪ η a → (∀ᵐ (b : β) ∂η a, κ.rnDeriv η a b = 1) → κ a = η a

Tactic:
h_ac

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝³ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h : μ ⊗ₘ κ = μ ⊗ₘ η
h_ac✝ : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ_eq : ∀ᵐ (a : α) ∂μ, κ a = (η.withDensity (κ.rnDeriv η)) a
this : ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂η a, κ.rnDeriv η a b = 1
a : α
h_ac : κ a ≪ η a
⊢ (∀ᵐ (b : β) ∂η a, κ.rnDeriv η a b = 1) → κ a = η a
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:

Tactic:
(Kernel.id ∥ₖ κ†μ) ∘ₘ Kernel.copy 𝓧 ∘ₘ κ ∘ₘ μ
  _ = (κ ∘ₘ μ) ⊗ₘ κ†μ := by rw [← Measure.compProd_eq_parallelComp_comp_copy_comp]
  _ = Kernel.swap _ _ ∘ₘ (μ ⊗ₘ κ) := by rw [compProd_posterior_eq_swap_comp]
  _ = Kernel.swap _ _ ∘ₘ (Kernel.id ∥ₖ κ) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    rw [Measure.compProd_eq_parallelComp_comp_copy_comp]
  _ = (κ ∥ₖ Kernel.id) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    rw [Measure.comp_assoc, Kernel.swap_parallelComp, Measure.comp_assoc, Kernel.comp_assoc,
      Kernel.swap_copy, Measure.comp_assoc]

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)
a b : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ Measure.map (frestrictLe b) ((traj κ a) x) = (partialTraj κ a b) x

Tactic:
← map_apply _ (measurable_frestrictLe b),

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)
a b : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ ((traj κ a).map (frestrictLe b)) x = (partialTraj κ a b) x
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 𝓨
⊢ ∀ (i : Kernel 𝓧 𝓨), IsMarkovKernel i → ⨅ y, ∫⁻ (θ : Θ), ℓ θ y * μ Set.univ ∂π ≤ avgRisk ℓ (Kernel.const Θ μ) i π

Tactic:
intro κ

Goal state after:
Θ : 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 𝓨
κ : Kernel 𝓧 𝓨
⊢ IsMarkovKernel κ → ⨅ y, ∫⁻ (θ : Θ), ℓ θ y * μ Set.univ ∂π ≤ avgRisk ℓ (Kernel.const Θ μ) κ π
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧},
    MeasurableSet s →
      MeasurableSet t →
        ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod (⇑κ ∘ₘ μ) = (μ ⊗ₘ κ) (s ×ˢ t)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
ω : Ω
⊢ κ ω ≪ ⇑κ ∘ₘ μ → ∫⁻ (y : 𝓧) in t, κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω y ∂⇑κ ∘ₘ μ = (κ ω) t

Tactic:
h_ac

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac✝ : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧},
    MeasurableSet s →
      MeasurableSet t →
        ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod (⇑κ ∘ₘ μ) = (μ ⊗ₘ κ) (s ×ˢ t)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
ω : Ω
h_ac : κ ω ≪ ⇑κ ∘ₘ μ
⊢ ∫⁻ (y : 𝓧) in t, κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω y ∂⇑κ ∘ₘ μ = (κ ω) t
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝² : DecidableEq ι
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ι) → X i) → E
mf : StronglyMeasurable f
x : (i : ι) → X i
g : ((i : ↥s) → X ↑i) → E := fun y ↦ f (Function.updateFinset x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict y) = f y
⊢ ∫ (y : (i : ι) → X i), f y ∂infinitePi μ =
    ∫ (y : (i : ↥s) → X ↑i), f (Function.updateFinset x s y) ∂Measure.pi fun i ↦ μ ↑i

Tactic:
← integral_congr_ae <| ae_of_all _ this,

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝² : DecidableEq ι
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ι) → X i) → E
mf : StronglyMeasurable f
x : (i : ι) → X i
g : ((i : ↥s) → X ↑i) → E := fun y ↦ f (Function.updateFinset x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict y) = f y
⊢ ∫ (a : (i : ι) → X i), g (s.restrict a) ∂infinitePi μ =
    ∫ (y : (i : ↥s) → X ↑i), f (Function.updateFinset x s y) ∂Measure.pi fun i ↦ μ ↑i
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : DecidableEq ι
s : Finset ι
f : ((i : ι) → X i) → ℝ≥0∞
mf : Measurable f
x : (i : ι) → X i
g : ((i : ↥s) → X ↑i) → ℝ≥0∞ := fun y ↦ f (Function.updateFinset x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict y) = f y
⊢ Measurable g

Tactic:
exact mf.comp (measurable_updateFinset.mono le_rfl (piFinset.le s))

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

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
η : Kernel 𝓧 𝓧'
inst✝ : IsMarkovKernel η
⊢ ∀ (i : Kernel 𝓧' 𝓨),
    IsMarkovKernel i →
      ⨅ κ, ⨅ (_ : IsMarkovKernel κ), ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ P) θ ∂π ≤
        ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(i ∘ₖ (η ∘ₖ P)) θ ∂π

Tactic:
intro κ

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
η : Kernel 𝓧 𝓧'
inst✝ : IsMarkovKernel η
κ : Kernel 𝓧' 𝓨
⊢ IsMarkovKernel κ →
    ⨅ κ, ⨅ (_ : IsMarkovKernel κ), ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ P) θ ∂π ≤
      ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ (η ∘ₖ P)) θ ∂π
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: x a r : ℝ
hx : x ≤ 0
⊢ ∫⁻ (x : ℝ) in Iio x, 0 = 0

Tactic:
lintegral_zero,

Goal state after:
x a r : ℝ
hx : x ≤ 0
⊢ 0 = 0
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: x a✝¹ r : ℝ
hx : x ≤ 0
a : ℝ
a✝ : a < x
⊢ (if 0 ≤ a then r ^ a✝¹ / Gamma a✝¹ * a ^ (a✝¹ - 1) * rexp (-(r * a)) else 0) ≤ 0

Tactic:
rw [if_neg (by linarith)]

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

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ ∫⁻ (x : ℝ) in Iic x, ?m.54 x = ENNReal.ofReal 0

pp: r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ EqOn (fun y ↦ ENNReal.ofReal (if 0 ≤ y then r * rexp (-(r * y)) else 0)) ?m.54 (Iic x)

pp: r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ ℝ → ℝ≥0∞

Tactic:
lintegral_zero,

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ 0 = ENNReal.ofReal 0

r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ EqOn (fun y ↦ ENNReal.ofReal (if 0 ≤ y then r * rexp (-(r * y)) else 0)) (fun x ↦ 0) (Iic x)
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
a : ℝ
x✝ : a ≤ x
⊢ ENNReal.ofReal (if 0 ≤ a then r * rexp (-(r * a)) else 0) = 0

Tactic:
rw [if_neg (by linarith), ENNReal.ofReal_eq_zero]

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

Goal state before:
pp: p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
f : ℕ → E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
⊢ (fun n ↦ ((1 - ↑p) ^ n * ↑p) • f n) = fun n ↦ (ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)).toReal • f n

Tactic:
ext n

Goal state after:
p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
f : ℕ → E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
n : ℕ
⊢ ((1 - ↑p) ^ n * ↑p) • f n = (ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)).toReal • f n
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r x : ℝ
hx : x ≤ t
⊢ ∫⁻ (x : ℝ) in Iio x, 0 = 0

Tactic:
lintegral_zero,

Goal state after:
t r x : ℝ
hx : x ≤ t
⊢ 0 = 0
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r x : ℝ
hx : x ≤ t
a : ℝ
a✝ : a < x
⊢ (if t ≤ a then r * t ^ r * a ^ (-(r + 1)) else 0) ≤ 0

Tactic:
rw [if_neg (by linarith)]

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

Goal state before:
pp: Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
⊢ μ[X | m] - μ[X | m] ^ 2 =ᵐ[μ] μ[X | m] * μ[1 - X | m]

Tactic:
rw [sq, ← one_sub_mul, mul_comm]
      refine .mul ae_eq_rfl ?_
      calc
        1 - μ[X | m]
        _ = μ[1 | m] - μ[X | m] := by simp [Pi.one_def, hm]
        _ =ᵐ[μ] μ[1 - X | m] := by
          refine (condExp_sub (integrable_const _)
            (.of_bound (C := 1) hXmeas.aestronglyMeasurable ?_) _).symm
          filter_upwards [hX]
          rintro ω (hω | hω) <;> simp [hω]

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

Goal state before:
pp: case hf
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ AEMeasurable (fun ω ↦ ω i) (infinitePi P)

pp: case hg
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ AEMeasurable (fun ω ↦ ω j) (infinitePi P)

Tactic:
all_goals exact Measurable.aemeasurable (by fun_prop)

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

Goal state before:
pp: case neg.refine_1
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
⊢ IntegrableOn (fun x ↦ ∫ (x : Ω), f x ∂μ[|s]) t (μ.restrict s)

Tactic:
rw [integrableOn_const_iff]

Goal state after:
case neg.refine_1
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
⊢ ‖∫ (x : Ω), f x ∂μ[|s]‖ₑ = 0 ∨ (μ.restrict s) t < ∞
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ π.IsProper ↔ ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x ↦ 1) x • π x

Tactic:
refine ⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨?_⟩⟩

Goal state after:
case refine_1
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
x✝ : π.IsProper
h : ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x ↦ 1) x • π x
⊢ ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x ↦ 1) x • π x

case refine_2
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
h : ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x ↦ 1) x • π x
⊢ ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x ↦ 1) x • π x
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: case refine_2
Ω : 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
n : ι
inst✝¹ : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
hτ_countable_range : (Set.range τ).Countable
hσ_countable_range : (Set.range σ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
this✝ : SigmaFinite (μ.trim ⋯)
this : μ[stoppedValue f τ | hσ.measurableSpace] =ᵐ[μ] μ[μ[f n | hτ.measurableSpace] | hσ.measurableSpace]
⊢ hσ.measurableSpace ≤ hτ.measurableSpace

Tactic:
exact hσ.measurableSpace_mono hτ hσ_le_τ

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✝¹ : IsProbabilityMeasure P
inst✝ : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : ((s : S) → E s) →ᵇ ℝ), ∫ (ω : Ω) in A, f fun x ↦ X x ω ∂P = P.real A * ∫ (ω : Ω), f fun x ↦ X x ω ∂P
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
⊢ ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P

Tactic:
convert! h (∏ s, (f s).compContinuous ⟨Function.eval s, by fun_prop⟩) <;> simp

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
g : G
x₁ : W
hx₁ : x₁ ∈ ρ₁.toSubmodule
x₂ : W
⊢ x₂ ∈ ρ₂.toSubmodule → (ρ g) x₁ + (ρ g) x₂ ∈ ρ₁.toSubmodule ⊔ ρ₂.toSubmodule

Tactic:
hx₂

Goal state after:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
g : G
x₁ : W
hx₁ : x₁ ∈ ρ₁.toSubmodule
x₂ : W
hx₂ : x₂ ∈ ρ₂.toSubmodule
⊢ (ρ g) x₁ + (ρ g) x₂ ∈ ρ₁.toSubmodule ⊔ ρ₂.toSubmodule
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case h₁
Ω : 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 := ⋯
q : ℝ≥0 := ⋯
ω' : Ω'
hmX : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑cX * t ^ 2 / 2)
hmY : ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑cY * t ^ 2 / 2)
hlX : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')
hlY : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * Y ω)) (↑q) (κ ω')
t : ℝ
⊢ ∫ (x : Ω), rexp (t * ↑p * X x) ∂κ ω' ≤ rexp (↑cX * (t * ↑p) ^ 2 / 2)

Tactic:
exact hmX (t * p)

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < P {ω | σ n k ω < min (τ n ω) ↑(T n)}
⊢ ∀ (i : ℕ), (1 / 2) ^ n ≤ P {ω | σ n i ω < min (τ n ω) ↑(T n)}

Tactic:
exact fun k ↦ (hn k).le

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
this : ∀ᵐ (x : ℝ) ∂Measure.map f μ, 0 ≤ x
x : ℝ
hx : 0 ≤ x
⊢ A < x → x ≤ 0 → x ^ n = 0

Tactic:
intro _ h''x

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
this : ∀ᵐ (x : ℝ) ∂Measure.map f μ, 0 ≤ x
x : ℝ
hx : 0 ≤ x
a✝ : A < x
h''x : x ≤ 0
⊢ x ^ n = 0
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case pos.inr.refine_2
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
⊢ MemLp (fun ω ↦ rexp (t * Y ω.2)) 2 (⇑(κ ⊗ₖ η) ∘ₘ ν)

Tactic:
have h := hY.memLp_exp_mul t 2
    rwa [ENNReal.coe_ofNat, Measure.comp_compProd_comm, Measure.snd,
      memLp_map_measure_iff h.1 measurable_snd.aemeasurable] at h

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
n : ℕ
⊢ ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ

Tactic:
change 𝔼[fun x => Y n x ^ 2] = _

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
n : ℕ
⊢ ∫ (a : Ω), (fun x ↦ Y n x ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
t : ℝ
⊢ mgf X μ t ≤ rexp (↑((‖b - a‖₊ / 2) ^ 2) * t ^ 2 / 2)

Tactic:
by
    obtain ht | ht | ht := lt_trichotomy 0 t
    · exact ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero hm hb hc ht
    · simp [← ht]
    calc
    _ = mgf (-X) μ (-t) := by simp [mgf]
    _ ≤ exp ((‖-a - -b‖₊ / 2) ^ 2 * (-t) ^ 2 / 2) := by
      apply ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero (hm.neg)
      · filter_upwards [hb] with ω ⟨hl, hr⟩ using ⟨neg_le_neg_iff.2 hr, neg_le_neg_iff.2 hl⟩
      · simp only [Pi.neg_apply]; rw [integral_neg, hc, neg_zero]
      · rwa [Left.neg_pos_iff]
    _ = exp (((‖b - a‖₊ / 2) ^ 2) * t ^ 2 / 2) := by ring_nf

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f : ρ.IntertwiningMap ρ
n : ℕ
⊢ (f ^ n).toLinearMap = f.toLinearMap ^ n

Tactic:
induction n with

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

Goal state before:
pp: case succ
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst✝ : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
hn :
  (∀ i < n - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ) →
    HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ
h_subG : ∀ i < n + 1 - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
⊢ HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ

Tactic:
induction n with

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst✝ : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
h_subG : ∀ i < n - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
⊢ HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ

Tactic:
induction n with

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e'_7
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ∞
B : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
ω : Ω
hω : Tendsto (fun n ↦ truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
⊢ (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) = fun n ↦
    ∑ i ∈ range n, (truncation (X i) (↑i) ω - X i ω)

Tactic:
ext n

Goal state after:
case e'_7
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ∞
B : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
ω : Ω
hω : Tendsto (fun n ↦ truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
n : ℕ
⊢ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω = ∑ i ∈ range n, (truncation (X i) (↑i) ω - X i ω)