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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : β → E
inst✝ : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
⊢ ∫ (b : β), f b ∂(κ.withDensity fun a b ↦ ↑(g a b)) a = ∫ (b : β), g a b • f b ∂κ a

Tactic:
Kernel.withDensity_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : β → E
inst✝ : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
⊢ (∫ (b : β), f b ∂(κ a).withDensity fun b ↦ ↑(g a b)) = ∫ (b : β), g a b • f b ∂κ a

case hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : β → E
inst✝ : IsSFiniteKernel κ
a : α
g : α → β → ℝ≥0
hg : Measurable (Function.uncurry g)
⊢ Measurable (Function.uncurry fun a b ↦ ↑(g a b))
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.withDensity (f + g)) a) s✝ = ((κ a).withDensity (f a) + (κ a).withDensity (g a)) s✝

Tactic:
Kernel.withDensity_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ a).withDensity ((f + g) a)) s✝ = ((κ a).withDensity (f a) + (κ a).withDensity (g a)) s✝

case hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ Measurable (Function.uncurry (f + g))
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0

Tactic:
singularPart,

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ (((κ + η).withDensity fun a x ↦
          ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x)
        a)
      (κ.mutuallySingularSetSlice η a)ᶜ =
    0
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ κ.mutuallySingularSetSlice η a
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
⊢ ((κ.singularPart η) a) s = (κ a) s

Tactic:
singularPart,

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ κ.mutuallySingularSetSlice η a
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
⊢ (((κ + η).withDensity fun a x ↦
          ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x)
        a)
      s =
    (κ a) s
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ ∫⁻ (z : (i : ↥(Iic b)) → X ↑i),
      f (updateFinset x₀ (Iic b) z) ∂(deterministic (frestrictLe₂ hba) ⋯) (frestrictLe a x₀) =
    f x₀

Tactic:
Kernel.lintegral_deterministic'

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ f (updateFinset x₀ (Iic b) (frestrictLe₂ hba (frestrictLe a x₀))) = f x₀

case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ Measurable fun z ↦ f (updateFinset x₀ (Iic b) z)
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 Θ 𝓧
inst✝² : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsMarkovKernel κ
π : Measure Θ
inst✝ : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
⊢ ↑C * κ.bound * P.bound * π Set.univ ≤ ↑C

Tactic:
rcases isEmpty_or_nonempty Θ

Goal state after:
case inl
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst✝² : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsMarkovKernel κ
π : Measure Θ
inst✝ : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
h✝ : IsEmpty Θ
⊢ ↑C * κ.bound * P.bound * π Set.univ ≤ ↑C

case inr
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst✝² : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsMarkovKernel κ
π : Measure Θ
inst✝ : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
h✝ : Nonempty Θ
⊢ ↑C * κ.bound * P.bound * π Set.univ ≤ ↑C
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∞
inst✝² : Nonempty 𝓨
P : Kernel Θ 𝓧
inst✝¹ : IsMarkovKernel P
π : Measure Θ
inst✝ : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
⊢ ↑C * P.bound * π Set.univ ≤ ↑C

Tactic:
rcases isEmpty_or_nonempty Θ

Goal state after:
case inl
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝² : Nonempty 𝓨
P : Kernel Θ 𝓧
inst✝¹ : IsMarkovKernel P
π : Measure Θ
inst✝ : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
h✝ : IsEmpty Θ
⊢ ↑C * P.bound * π Set.univ ≤ ↑C

case inr
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝² : Nonempty 𝓨
P : Kernel Θ 𝓧
inst✝¹ : IsMarkovKernel P
π : Measure Θ
inst✝ : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
h✝ : Nonempty Θ
⊢ ↑C * P.bound * π Set.univ ≤ ↑C
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 : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
⊢ ∀ᵐ (x : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) x = μ.withDensity fun ω ↦ κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x

Tactic:
by
  filter_upwards [rnDeriv_posterior_symm h_ac, absolutelyContinuous_posterior h_ac] with x h h_ac'
  ext s hs
  rw [← Measure.setLIntegral_rnDeriv h_ac', withDensity_apply _ hs]
  refine setLIntegral_congr_fun_ae hs ?_
  filter_upwards [h, Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ†μ) (η := Kernel.const 𝓧 μ) (a := x)]
    with ω h h_eq hωs
  rw [← h, h_eq, Kernel.const_apply]

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)))
⊢ r * t ^ r * ∫ (a : ℝ) in Ioi t, a ^ (-(r + 1)) = 1

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

Goal state before:
pp: case pos
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : volume s = 0 ∨ volume s = ∞
⊢ Integrable (fun x ↦ x * (pdf X ℙ volume x).toReal) volume

pp: case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬(volume s = 0 ∨ volume s = ∞)
⊢ Integrable (fun x ↦ x * (pdf X ℙ volume x).toReal) volume

Tactic:
· have I : Integrable (fun x ↦ x * ENNReal.toReal (0)) := by simp
    apply I.congr
    filter_upwards [pdf_eq_zero_of_measure_eq_zero_or_top huX hnt] with x hx
    simp [hx]

Goal state after:
case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬(volume s = 0 ∨ volume s = ∞)
⊢ Integrable (fun x ↦ x * (pdf X ℙ volume x).toReal) volume
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
⊢ ⇑(condExpKernel μ m) ∘ₘ μ.trim hm = μ

Tactic:
by
  rw [← Measure.snd_compProd, compProd_trim_condExpKernel]
  exact (@Measure.snd_map_prodMk Ω Ω Ω mΩ m mΩ id id μ (measurable_id'' hm)).trans Measure.map_id

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Ω
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ i ∈ s, (fun ω ↦ (((condExpKernel μ m') ω) (f i)).toReal) =ᵐ[μ] μ[(f i).indicator fun ω ↦ 1 | m']
h_eq :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = μ[(f i).indicator fun ω ↦ 1 | m'] ω
s : Finset ι
f : ι → Set Ω
H : ∀ i ∈ s, f i ∈ π i
⊢ MeasurableSet (⋂ i ∈ s, f i)

Tactic:
exact MeasurableSet.biInter (Finset.countable_toSet _) (fun i hi ↦ hπ i _ (H i hi))

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

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
a✝ : PUnit.{u + 1} × X✝.carrier
s✝ : Set Y✝.carrier
hs : MeasurableSet s✝
this : IsSFiniteKernel κ.hom
⊢ ((Kernel.id ∥ₖ κ.hom) a✝) (Prod.snd ⁻¹' s✝) = (κ.hom a✝.2) s✝

Tactic:
Kernel.parallelComp_apply' <| measurable_snd hs

Goal state after:
X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
a✝ : PUnit.{u + 1} × X✝.carrier
s✝ : Set Y✝.carrier
hs : MeasurableSet s✝
this : IsSFiniteKernel κ.hom
⊢ ∫⁻ (b : PUnit.{u + 1}), (κ.hom a✝.2) (Prod.mk b ⁻¹' Prod.snd ⁻¹' s✝) ∂Kernel.id a✝.1 = (κ.hom a✝.2) s✝
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case e'_2
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ (μ.trim hm' ⊗ₘ (condExpKernel μ m').map fun ω ↦ (f ω, g ω)) = Measure.map (fun ω ↦ (ω, f ω, g ω)) μ

Tactic:
rw [Measure.compProd_map (by fun_prop), compProd_trim_condExpKernel]

Goal state after:
case e'_2
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ Measure.map (Prod.map id fun ω ↦ (f ω, g ω)) (Measure.map Function.diag μ) = Measure.map (fun ω ↦ (ω, f ω, g ω)) μ
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
sSup_eq_iUnion_rat :
  {x | a < f x.1 x.2} = ⋃ q, ⋃ (hqI : ↑q ∈ I), ⋃ (_ : ↑a < ↑q), {e | (κ e.1).real (Icc 0 ⟨↑q, hqI⟩) < ↑e.2}
b : ℚ
bI : ↑b ∈ I
x✝ : ↑a < ↑b
⊢ Measurable fun e ↦ ((κ e.1) (Icc 0 ⟨↑b, bI⟩)).toReal

Tactic:
have hκ := κ.measurable_coe (s := Icc 0 ⟨b, bI⟩) measurableSet_Icc

Goal state after:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
sSup_eq_iUnion_rat :
  {x | a < f x.1 x.2} = ⋃ q, ⋃ (hqI : ↑q ∈ I), ⋃ (_ : ↑a < ↑q), {e | (κ e.1).real (Icc 0 ⟨↑q, hqI⟩) < ↑e.2}
b : ℚ
bI : ↑b ∈ I
x✝ : ↑a < ↑b
hκ : Measurable fun a ↦ (κ a) (Icc 0 ⟨↑b, bI⟩)
⊢ Measurable fun e ↦ ((κ e.1) (Icc 0 ⟨↑b, bI⟩)).toReal
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ ε = (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ SFinKer)).hom

Tactic:
ext : 1; dsimp
    simp only [Kernel.id_parallelComp_comp_parallelComp_id]
    rw [Kernel.id_map (by fun_prop), Kernel.deterministic_comp_eq_map]
    ext
    rw [Kernel.map_apply _ (by fun_prop), Kernel.parallelComp_apply]
    simp [Kernel.discard_apply]

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

Goal state before:
pp: case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : Ω → E
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ (∫ (ω : Ω), g ω ∂μ.tilted fun x ↦ t * X x) = ∫ (ω : Ω), rexp (t * X ω - cgf X μ t) • g ω ∂μ

Tactic:
integral_tilted_mul_eq_mgf,

Goal state after:
case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : Ω → E
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ = ∫ (ω : Ω), rexp (t * X ω - cgf X μ t) • g ω ∂μ
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ (∫ (x : Ω), X x ∂μ.tilted fun x ↦ t * X x) = deriv (cgf X μ) t

Tactic:
integral_tilted_mul_eq_mgf,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ ∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • X ω ∂μ = deriv (cgf X μ) t
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ (∫ (ω : Ω), (X ω - deriv (cgf X μ) t) ^ 2 ∂μ.tilted fun x ↦ t * X x) =
    (∫ (x : Ω), (fun ω ↦ (X ω - deriv (cgf X μ) t) ^ 2 * rexp (t * X ω)) x ∂μ) / mgf X μ t

Tactic:
integral_tilted_mul_eq_mgf,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ ∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • (X ω - deriv (cgf X μ) t) ^ 2 ∂μ =
    (∫ (x : Ω), (fun ω ↦ (X ω - deriv (cgf X μ) t) ^ 2 * rexp (t * X ω)) x ∂μ) / mgf X μ t
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 κ ν
⊢ X =ᵐ[⇑κ ∘ₘ ν] 0

Tactic:
by
  have hX := h.aestronglyMeasurable
  have h' : HasSubgaussianMGF (hX.mk X) 0 κ ν := h.congr hX.ae_eq_mk
  exact hX.ae_eq_mk.trans (ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurable hX.measurable_mk h')

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

Goal state before:
pp: case hs
ι : 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)}
⊢ ∀ᵐ (ω : Ω) ∂P, Antitone fun x ↦ ω ∈ {ω | σ n x ω < min (τ n ω) ↑(T n)}

Tactic:
filter_upwards [(hσ n).mono] with ω hω

Goal state after:
ι : 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)}
ω : Ω
hω : Monotone fun x ↦ σ n x ω
⊢ Antitone fun x ↦ σ n x ω < min (τ n ω) ↑(T n)
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
nk : ℕ → ℕ
hnk : ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
n : ℕ
⊢ {ω | σ n (mkStrictMonoAux nk n) ω < min (τ n ω) ↑(T n)} ≤ᵐ[P] {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)}

Tactic:
filter_upwards [(hσ n).mono] with ω hω

Goal state after:
ι : 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
nk : ℕ → ℕ
hnk : ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
n : ℕ
ω : Ω
hω : Monotone fun x ↦ σ n x ω
⊢ {ω | σ n (mkStrictMonoAux nk n) ω < min (τ n ω) ↑(T n)} ω ≤ {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ω
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
A : Tendsto (fun N ↦ ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N}) atTop (𝓝 (∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j}))
⊢ ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)

Tactic:
apply le_of_tendsto_of_tendsto A tendsto_const_nhds

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
A : Tendsto (fun N ↦ ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N}) atTop (𝓝 (∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j}))
⊢ (fun N ↦ ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N}) ≤ᶠ[atTop] fun x ↦ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: case e_f
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁸ : ConditionallyCompleteLinearOrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : IsFiniteMeasure P
inst✝³ : DenselyOrdered ι
inst✝² : NoMaxOrder ι
inst✝¹ : Zero E
inst✝ : 𝓕.IsRightContinuous
hp : IsStable 𝓕 p
hL : Locally (fun Y ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : ℕ → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun i ↦
          {ω | ⊥ < τ n n_1 ω}.indicator
            (stoppedProcess (fun i ↦ {ω | ⊥ < hL.localSeq n ω}.indicator (X i)) (hL.localSeq n) i))
        (τ n n_1))
nk : ℕ → ℕ
hnk : StrictMono nk
hpre : IsPreLocalizingSequence 𝓕 (fun i ω ↦ min (hL.localSeq i ω) (τ i (nk i) ω)) P
n : ℕ
i : ι
ω : Ω
⊢ stoppedProcess X (fun ω ↦ min (hL.localSeq n ω) (τ n (nk n) ω)) i = stoppedProcess X (τ n (nk n) ⊓ hL.localSeq n) i

Tactic:
simp_rw [inf_comm]
    rfl

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
h_eq : μ[fun ω ↦ rexp (t * X ω) | m] =ᵐ[μ.trim hm] fun ω ↦ ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel μ m) ω
⊢ ∀ᵐ (ω' : Ω) ∂μ.trim hm, μ[fun ω ↦ rexp (t * X ω) | m] ω' ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
filter_upwards [h.mgf_le, h_eq] with ω' h_mgf h_eq

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
h_eq✝ : μ[fun ω ↦ rexp (t * X ω) | m] =ᵐ[μ.trim hm] fun ω ↦ ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel μ m) ω
ω' : Ω
h_mgf : ∀ (t : ℝ), mgf X ((condExpKernel μ m) ω') t ≤ rexp (↑c * t ^ 2 / 2)
h_eq : μ[fun ω ↦ rexp (t * X ω) | m] ω' = ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel μ m) ω'
⊢ μ[fun ω ↦ rexp (t * X ω) | m] ω' ≤ rexp (↑c * t ^ 2 / 2)
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
a : A
f : σ.IntertwiningMap τ
g : ρ.IntertwiningMap σ
⊢ (a • f).comp g = a • f.comp g

Tactic:
simp [comp_def]

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
a : A
f : σ.IntertwiningMap τ
g : ρ.IntertwiningMap σ
⊢ f.comp (a • g) = a • f.comp g

Tactic:
simp [comp_def]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case hident
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := ⋯
F_meas : Measurable F
Y : ℕ → Ω → ℝ := ⋯
⊢ ∀ (i : ℕ), IdentDistrib (Y i) (Y 0) μ μ

Tactic:
· exact fun i ↦ (hident i).comp F_meas

Goal state after: