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

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n ↦ fs n a
a : α
b : β
⊢ ∑ i ∈ Finset.range 0, fs i a b = min (f a b) ↑0

Tactic:
| zero =>

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

Goal state before:
pp: case hfg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
⊢ ∀ (a : α), (fun x ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) ≤ᵐ[(κ + η) a] fun x ↦ 1

Tactic:
intro a

Goal state after:
case hfg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
a : α
⊢ (fun x ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) ≤ᵐ[(κ + η) a] fun x ↦ 1
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 η
a : α
h_eq_add : ∀ (a : α) (s : Set γ), MeasurableSet s → ((η.withDensity (κ.rnDeriv η) + κ.singularPart η) a) s = (κ a) s
⊢ (κ.singularPart η) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a) = 0

Tactic:
specialize h_eq_add a (mutuallySingularSetSlice κ η a)
    (measurableSet_mutuallySingularSetSlice κ η a)

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h_eq_add :
  ((η.withDensity (κ.rnDeriv η) + κ.singularPart η) a) (κ.mutuallySingularSetSlice η a) =
    (κ a) (κ.mutuallySingularSetSlice η a)
⊢ (κ.singularPart η) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a) = 0
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 : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ (trajContent κ x₀) (cylinder (Iic 0) Set.univ) = 1

pp: case hC_gen
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ MeasurableSpace.pi = generateFrom (measurableCylinders X)

pp: case hs
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ cylinder (Iic 0) Set.univ ∈ measurableCylinders X

Tactic:
trajContent_cylinder .univ,

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 : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ ((partialTraj κ a 0) x₀) Set.univ = 1

case hC_gen
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ MeasurableSpace.pi = generateFrom (measurableCylinders X)

case hs
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ cylinder (Iic 0) Set.univ ∈ measurableCylinders 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∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝² : Subsingleton 𝓧
inst✝¹ : Nonempty 𝓨
inst✝ : SFinite π
hl : Measurable (uncurry ℓ)
⊢ bayesRisk ℓ P π = ⨅ y, ∫⁻ (θ : Θ), ℓ θ y * (P θ) Set.univ ∂π

Tactic:
by
  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.Distributions.Gamma

Goal state before:
pp: x a r : ℝ
hx : x ≤ 0
⊢ EqOn (gammaPDF a r) (fun x ↦ 0) (Iio x)

Tactic:
intro a

Goal state after:
x a✝ r : ℝ
hx : x ≤ 0
a : ℝ
⊢ a ∈ Iio x → gammaPDF a✝ r a = (fun x ↦ 0) a
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ EqOn (fun x ↦ ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0))
    (fun x ↦ ENNReal.ofReal (r * rexp (-(r * x)))) (Icc 0 x)

Tactic:
intro a

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
a : ℝ
⊢ a ∈ Icc 0 x →
    (fun x ↦ ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0)) a =
      (fun x ↦ ENNReal.ofReal (r * rexp (-(r * x)))) a
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r x : ℝ
hx : x ≤ t
⊢ EqOn (paretoPDF t r) (fun x ↦ 0) (Iio x)

Tactic:
intro a

Goal state after:
t r x : ℝ
hx : x ≤ t
a : ℝ
⊢ a ∈ Iio x → paretoPDF t r a = (fun x ↦ 0) a
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
⊢ 0 < paretoPDFReal t r x

Tactic:
by
  rw [paretoPDFReal, if_pos hx]
  have _ : 0 < x := by linarith
  positivity

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

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ ∫ (a : ℝ) in Ici t, r * t ^ r * a ^ (-(r + 1)) = 1

Tactic:
rw [integral_Ici_eq_integral_Ioi, integral_const_mul, integral_Ioi_rpow_of_lt _ ht]

Goal state after:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ r * t ^ r * (-t ^ (-(r + 1) + 1) / (-(r + 1) + 1)) = 1

t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ -(r + 1) < -1
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
b : Bool
⊢ b ∈ (bernoulli p h).support ↔ bif b then p ≠ 0 else p ≠ 1

Tactic:
simp [support_bernoulli]

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

Goal state before:
pp: case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ∞
this✝ : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := (volume s)⁻¹ • 1
this : ∀ (x : ℝ), ‖x‖ₑ * s.indicator ind x = s.indicator (fun x ↦ ‖x‖ₑ * ind x) x
⊢ ∫⁻ (x : ℝ) in s, ‖x‖ₑ * (volume s)⁻¹ ∂volume ≠ ∞

Tactic:
rw [lintegral_mul_const _ measurable_enorm]

Goal state after:
case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ∞
this✝ : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := (volume s)⁻¹ • 1
this : ∀ (x : ℝ), ‖x‖ₑ * s.indicator ind x = s.indicator (fun x ↦ ‖x‖ₑ * ind x) x
⊢ (∫⁻ (a : ℝ) in s, ‖a‖ₑ ∂volume) * (volume s)⁻¹ ≠ ∞
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: case refine_1
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
⊢ iIndepFun (fun i ω x ↦ X i x (ω i x)) (infinitePi fun i ↦ infinitePi (μ i))

pp: case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ iIndepFun (fun j ω ↦ X i j (ω i j)) (infinitePi fun i ↦ infinitePi (μ i))

Tactic:
· exact iIndepFun_infinitePi (P := fun i ↦ infinitePi (μ i))
      (X := fun i u j ↦ X i j (u j)) (by fun_prop)

Goal state after:
case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ iIndepFun (fun j ω ↦ X i j (ω i j)) (infinitePi fun i ↦ infinitePi (μ i))
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: case inr.hm
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ⨆ n ∈ ns i, s n

Tactic:
intro a

Goal state after:
case inr.hm
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
a : β
⊢ ∀ (y : β),
    ∃ z,
      (fun x1 x2 ↦ x1 ≤ x2) ((fun i ↦ ⨆ n ∈ ns i, s n) a) ((fun i ↦ ⨆ n ∈ ns i, s n) z) ∧
        (fun x1 x2 ↦ x1 ≤ x2) ((fun i ↦ ⨆ n ∈ ns i, s n) y) ((fun i ↦ ⨆ n ∈ ns i, s n) z)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_1
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ (Kernel.deterministic Prod.snd hf₂).map f₁ = Kernel.id

Tactic:
Kernel.deterministic_map hf₂ hf₁

Goal state after:
case refine_1
X : SFinKer
f₁ : X.carrier → PUnit.{u + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.snd
⊢ Kernel.deterministic (f₁ ∘ Prod.snd) ⋯ = Kernel.id
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_1
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ (Kernel.deterministic Prod.fst hf₂).map f₁ = Kernel.id

Tactic:
Kernel.deterministic_map hf₂ hf₁

Goal state after:
case refine_1
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ Kernel.deterministic (f₁ ∘ Prod.fst) ⋯ = Kernel.id
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f' : ℕ → X → ℝ≥0∞
hf'_meas : ∀ (n : ℕ), Measurable (f' n)
hf'_mono : Monotone f'
hf' : ∀ (n : ℕ), ∫⁻ (x : X), B.indicator 1 x * f' n x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f' n x ∂π x₀
⊢ ∫⁻ (x : X), B.indicator 1 x * ⨆ n, f' n x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), ⨆ n, f' n x ∂π x₀

Tactic:
ENNReal.mul_iSup

Goal state after:
case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f' : ℕ → X → ℝ≥0∞
hf'_meas : ∀ (n : ℕ), Measurable (f' n)
hf'_mono : Monotone f'
hf' : ∀ (n : ℕ), ∫⁻ (x : X), B.indicator 1 x * f' n x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f' n x ∂π x₀
⊢ ∫⁻ (x : X), ⨆ i, B.indicator 1 x * f' i x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), ⨆ n, f' n x ∂π x₀
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f' : ℕ → X → ℝ≥0∞
hf'_meas : ∀ (n : ℕ), Measurable (f' n)
hf'_mono : Monotone f'
hf' : ∀ (n : ℕ), ∫⁻ (x : X), B.indicator 1 x * f' n x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f' n x ∂π x₀
⊢ ⨆ n, ∫⁻ (a : X), B.indicator 1 a * f' n a ∂π x₀ = B.indicator 1 x₀ * ⨆ n, ∫⁻ (a : X), f' n a ∂π x₀

pp: case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f' : ℕ → X → ℝ≥0∞
hf'_meas : ∀ (n : ℕ), Measurable (f' n)
hf'_mono : Monotone f'
hf' : ∀ (n : ℕ), ∫⁻ (x : X), B.indicator 1 x * f' n x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f' n x ∂π x₀
⊢ Monotone fun i x ↦ B.indicator 1 x * f' i x

Tactic:
ENNReal.mul_iSup

Goal state after:
case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f' : ℕ → X → ℝ≥0∞
hf'_meas : ∀ (n : ℕ), Measurable (f' n)
hf'_mono : Monotone f'
hf' : ∀ (n : ℕ), ∫⁻ (x : X), B.indicator 1 x * f' n x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f' n x ∂π x₀
⊢ ⨆ n, ∫⁻ (a : X), B.indicator 1 a * f' n a ∂π x₀ = ⨆ i, B.indicator 1 x₀ * ∫⁻ (a : X), f' i a ∂π x₀

case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f' : ℕ → X → ℝ≥0∞
hf'_meas : ∀ (n : ℕ), Measurable (f' n)
hf'_mono : Monotone f'
hf' : ∀ (n : ℕ), ∫⁻ (x : X), B.indicator 1 x * f' n x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f' n x ∂π x₀
⊢ Monotone fun i x ↦ B.indicator 1 x * f' i x
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst✝² : Nonempty Y
mY : MeasurableSpace Y
inst✝¹ : StandardBorelSpace Y
κ : Kernel X Y
inst✝ : IsMarkovKernel κ
g : Y → ↑I := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (κ.map g)
⊢ κ = (κ.map g).map hg.invFun

Tactic:
← map_comp_right _ hg.measurable (by fun_prop),

Goal state after:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst✝² : Nonempty Y
mY : MeasurableSpace Y
inst✝¹ : StandardBorelSpace Y
κ : Kernel X Y
inst✝ : IsMarkovKernel κ
g : Y → ↑I := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (κ.map g)
⊢ κ = κ.map (hg.invFun ∘ sigmoid ∘ embeddingReal Y)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case neg
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
hp : ¬p = 0
⊢ eLpNorm (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω') < ∞

Tactic:
eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (mod_cast hp) (by simp),

Goal state after:
case neg
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
hp : ¬p = 0
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p).toReal ∂κ ω' < ∞
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 κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf (-X) (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
filter_upwards [h.mgf_le] with ω' hm t using by simpa [mgf] using hm (-t)

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
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᵐ[⇑κ ∘ₘ ν] Y
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * Y ω)) (⇑κ ∘ₘ ν)

Tactic:
refine (integrable_congr ?_).mpr (h.integrable_exp_mul t)

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᵐ[⇑κ ∘ₘ ν] Y
t : ℝ
⊢ (fun ω ↦ rexp (t * Y ω)) =ᵐ[⇑κ ∘ₘ ν] fun ω ↦ rexp (t * X ω)
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 κ ν
hs : {ω | 0 < X ω} = ⋃ ε, {ω | ↑↑ε ≤ X ω}
ε : ℚ
ω' : Ω'
a✝ : IsFiniteMeasure (κ ω')
hε : 0 < ε
hm : ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ↑ε ≤ X ω} ≤ rexp (-(t * ↑ε))
this : (κ ω').real {ω | ↑ε ≤ X ω} = 0
⊢ (κ ω') {ω | ↑ε ≤ X ω} = 0

Tactic:
simpa [Measure.real, ENNReal.toReal_eq_zero_iff]

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: case zero
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
σ : Subrepresentation ρ
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
⊢ 0 • v ∈ σ.toSubmodule.carrier

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: case zero
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
σ : Subrepresentation (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
⊢ 0 • m ∈ σ.toSubmodule.carrier

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case inr
α : 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
⊢ ∫ (x : α), (fun z ↦ (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ = ∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ

Tactic:
rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_ge hA.le,
      ← integral_indicator M']
    · simp only [Set.Ioc_eq_empty_of_le hA.le, zero_pow hn, Set.indicator_empty, integral_zero,
        zero_eq_neg]
      apply integral_eq_zero_of_ae
      have : ∀ᵐ x ∂Measure.map f μ, (0 : ℝ) ≤ x :=
        (ae_map_iff hf.aemeasurable measurableSet_Ici).2 (Eventually.of_forall h'f)
      filter_upwards [this] with x hx
      simp only [indicator, Set.mem_Ioc, Pi.zero_apply, ite_eq_right_iff, and_imp]
      intro _ h''x
      have : x = 0 := by linarith
      simp [this, zero_pow hn]
    · exact ((measurable_id.indicator M).pow_const n).aestronglyMeasurable

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h.hab
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := ⋯
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
⊢ ↑i ≤ ↑i + 1

Tactic:
simp only [le_add_iff_nonneg_right, zero_le_one]

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 N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∑ i ∈ range N, (↑i + 1) * ∫ (x : ℝ) in ↑i..↑(i + 1), 1 ∂ρ ≤ ∑ i ∈ range N, ∫ (x : ℝ) in ↑i..↑(i + 1), x + 1 ∂ρ

Tactic:
by
        gcongr with i
        have I : (i : ℝ) ≤ (i + 1 : ℕ) := by
          simp only [Nat.cast_add, Nat.cast_one, le_add_iff_nonneg_right, zero_le_one]
        simp_rw [intervalIntegral.integral_of_le I, ← integral_const_mul]
        apply setIntegral_mono_on
        · exact continuous_const.integrableOn_Ioc
        · exact (continuous_id.add continuous_const).integrableOn_Ioc
        · exact measurableSet_Ioc
        · intro x hx
          simp only [Nat.cast_add, Nat.cast_one, Set.mem_Ioc] at hx
          simp [hx.1.le]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h₂
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ρ.real (Set.Ioc 0 ↑N) ≤ ENNReal.toReal 1

Tactic:
exact ENNReal.toReal_mono ENNReal.one_ne_top prob_le_one

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 N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1
⊢ ∀ (a b : ℝ), ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)

Tactic:
intro a

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1
a : ℝ
⊢ ∀ (b : ℝ), ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1
B : ∀ (a b : ℝ), ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
j : ℕ
hj : j ∈ range K
⊢ ∫ (x : ℝ) in Set.Ioc ↑j ↑N, 1 ∂ρ = ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ

Tactic:
intervalIntegral.integral_of_le (Nat.cast_le.2 ((mem_range.1 hj).le.trans hKN))

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1
B : ∀ (a b : ℝ), ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
j : ℕ
hj : j ∈ range K
⊢ ∫ (x : ℝ) in Set.Ioc ↑j ↑N, 1 ∂ρ = ∫ (x : ℝ) in Set.Ioc ↑j ↑N, 1 ∂ρ