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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
integral_le_kernel : ∫⁻ (b : β) in t, (η b) s ∂κ a ≤ (κ a) t
⊢ ∫⁻ (x : β), (η x) sᶜ ∂κ a = ((η ∘ₖ κ) a) sᶜ

Tactic:
rw [η.comp_apply' _ _ hs.compl]

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)
n : ℕ
x : (i : ↥(Iic n)) → X ↑i
this : (fun x_1 ↦ updateFinset x_1 (Iic n) x) = ⇑(IicProdIoi n) ∘ Prod.mk x ∘ (Set.Ioi n).domRestrict
⊢ Measure.map (fun x_1 ↦ updateFinset x_1 (Iic n) x) ((traj κ n) x) =
    ((Kernel.id ×ₖ (traj κ n).map (Set.Ioi n).domRestrict).map ⇑(IicProdIoi n)) x

Tactic:
rw [this, ← Function.comp_assoc, ← Measure.map_map, ← Measure.map_map, map_apply, prod_apply,
    map_apply, id_apply, Measure.dirac_prod]

Goal state after:
case hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X ↑i
this : (fun x_1 ↦ updateFinset x_1 (Iic n) x) = ⇑(IicProdIoi n) ∘ Prod.mk x ∘ (Set.Ioi n).domRestrict
⊢ Measurable (Set.Ioi n).domRestrict

case hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X ↑i
this : (fun x_1 ↦ updateFinset x_1 (Iic n) x) = ⇑(IicProdIoi n) ∘ Prod.mk x ∘ (Set.Ioi n).domRestrict
⊢ Measurable ⇑(IicProdIoi n)

case hg
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X ↑i
this : (fun x_1 ↦ updateFinset x_1 (Iic n) x) = ⇑(IicProdIoi n) ∘ Prod.mk x ∘ (Set.Ioi n).domRestrict
⊢ Measurable ⇑(IicProdIoi n)

case hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X ↑i
this : (fun x_1 ↦ updateFinset x_1 (Iic n) x) = ⇑(IicProdIoi n) ∘ Prod.mk x ∘ (Set.Ioi n).domRestrict
⊢ Measurable (Prod.mk x)

case hg
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X ↑i
this : (fun x_1 ↦ updateFinset x_1 (Iic n) x) = ⇑(IicProdIoi n) ∘ Prod.mk x ∘ (Set.Ioi n).domRestrict
⊢ Measurable (⇑(IicProdIoi n) ∘ Prod.mk x)

case hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X ↑i
this : (fun x_1 ↦ updateFinset x_1 (Iic n) x) = ⇑(IicProdIoi n) ∘ Prod.mk x ∘ (Set.Ioi n).domRestrict
⊢ Measurable (Set.Ioi n).domRestrict
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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f :
  (∀ᵐ (y : (i : ↥(Iic b)) → X ↑i) ∂(partialTraj κ a b) x₀, Integrable f ((traj κ b) y)) ∧
    Integrable (fun y ↦ ∫ (z : (n : ℕ) → X n), ‖f z‖ ∂(traj κ b) y) ((partialTraj κ a b) x₀)
⊢ Measure.map (frestrictLe b) ((traj κ a) x₀) = ((traj κ a).map (frestrictLe b)) x₀

Tactic:
Kernel.map_apply _ (measurable_frestrictLe _)

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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f :
  (∀ᵐ (y : (i : ↥(Iic b)) → X ↑i) ∂(partialTraj κ a b) x₀, Integrable f ((traj κ b) y)) ∧
    Integrable (fun y ↦ ∫ (z : (n : ℕ) → X n), ‖f z‖ ∂(traj κ b) y) ((partialTraj κ a b) x₀)
⊢ Measure.map (frestrictLe b) ((traj κ a) x₀) = Measure.map (frestrictLe b) ((traj κ a) x₀)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case e_f
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 : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ ((traj κ b) x) (Prod.mk x ⁻¹' s) = ((traj κ b) x) ((fun x ↦ (frestrictLe b x, x)) ⁻¹' s)

Tactic:
rw [← traj_map_updateFinset, Measure.map_apply, Measure.map_apply]

Goal state after:
case e_f
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 : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ ((traj κ b) x) ((fun x_1 ↦ updateFinset x_1 (Iic b) x) ⁻¹' Prod.mk x ⁻¹' s) =
    ((traj κ b) x) ((fun x_1 ↦ updateFinset x_1 (Iic b) x) ⁻¹' (fun x ↦ (frestrictLe b x, x)) ⁻¹' s)

case e_f.hf
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 : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ Measurable fun x_1 ↦ updateFinset x_1 (Iic b) x

case e_f.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 b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ MeasurableSet ((fun x ↦ (frestrictLe b x, x)) ⁻¹' s)

case e_f.hf
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 : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ Measurable fun x_1 ↦ updateFinset x_1 (Iic b) x

case e_f.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 b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ MeasurableSet (Prod.mk x ⁻¹' s)
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 ha

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
a : ℝ
ha : 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.Geometric

Goal state before:
pp: p : ↑unitInterval
hp : p ≠ 0
⊢ HasSum (fun n ↦ (1 - ↑p) ^ n * ↑p) 1

Tactic:
by
  convert! (hasSum_geometric_of_lt_one (r := 1 - p) (by grind) (by grind)).mul_right (p : ℝ)
  grind

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

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

Tactic:
rw [ENNReal.toReal_ofReal_eq_iff.2
          (sub_nonneg.2 (Real.exp_le_one_iff.2 <| by nlinarith))]
        norm_num; ring

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

Goal state before:
pp: case false.mp
p : ℝ≥0
h : p ≤ 1
⊢ 1 - ↑p = 0 → p = 1

Tactic:
intro h'

Goal state after:
case false.mp
p : ℝ≥0
h : p ≤ 1
h' : 1 - ↑p = 0
⊢ p = 1
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: case false.mpr
p : ℝ≥0
h : p ≤ 1
⊢ p = 1 → 1 - ↑p = 0

Tactic:
intro h'

Goal state after:
case false.mpr
p : ℝ≥0
h : p ≤ 1
h' : p = 1
⊢ 1 - ↑p = 0
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
b : β
⊢ (if b ∈ s then ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) b else 0) =
    ∑' (a : α), if b ∈ s then p a * if h : p a = 0 then 0 else (f a h) b else 0

Tactic:
by split_ifs with hbs <;> simp only [tsum_zero]

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

Goal state before:
pp: case neg
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬μ s = ∞
hns : ¬μ s = 0
this✝ : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ Measure.map X ℙ = μ.withDensity (s.indicator ((μ s)⁻¹ • 1))

Tactic:
rw [hu, withDensity_indicator hms, withDensity_smul _ measurable_one, withDensity_one,
      ProbabilityTheory.cond]

Goal state after:
Module: Mathlib.Probability.IdentDistribIndep

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝ : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun X μ
hY_ind : iIndepFun Y ν
this✝ : IsProbabilityMeasure μ
this : IsProbabilityMeasure ν
⊢ (Measure.infinitePi fun i ↦ Measure.map (X i) μ) = Measure.infinitePi fun i ↦ Measure.map (Y i) ν

Tactic:
congr with i

Goal state after:
Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝ : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun X μ
hY_ind : iIndepFun Y ν
this✝ : IsProbabilityMeasure μ
this : IsProbabilityMeasure ν
i : ι
s✝ : Set (E i)
a✝ : MeasurableSet s✝
⊢ (Measure.map (X i) μ) s✝ = (Measure.map (Y i) ν) s✝
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
⊢ AEStronglyMeasurable (fun ω ↦ ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ

Tactic:
condExpKernel_eq

Goal state after:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
⊢ AEStronglyMeasurable (fun ω ↦ ∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω) μ
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ ∀ᵐ (ω : Ω) ∂μ, Integrable f ((condExpKernel μ m) ω)

Tactic:
condExpKernel_eq

Goal state after:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ ∀ᵐ (ω : Ω) ∂μ, Integrable f (((condDistrib id id μ).comap id ⋯) ω)
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω ↦ ∫ (y : Ω), ‖f y‖ ∂(condExpKernel μ m) ω) μ

Tactic:
condExpKernel_eq

Goal state after:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω ↦ ∫ (y : Ω), ‖f y‖ ∂((condDistrib id id μ).comap id ⋯) ω) μ
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω ↦ ‖∫ (y : Ω), f y ∂(condExpKernel μ m) ω‖) μ

Tactic:
condExpKernel_eq

Goal state after:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω ↦ ‖∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω‖) μ
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω ↦ ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ

Tactic:
condExpKernel_eq

Goal state after:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω ↦ ∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω) μ
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
a✝ : Nontrivial Ω
⊢ Integrable (fun ω ↦ ((condExpKernel μ m) ω).real s) μ

Tactic:
condExpKernel_eq

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
a✝ : Nontrivial Ω
⊢ Integrable (fun ω ↦ (((condDistrib id id μ).comap id ⋯) ω).real s) μ
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: case refine_2
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₂ ∘ₖ Kernel.id.map f₁ = Kernel.id

Tactic:
Kernel.deterministic_comp_eq_map hf₂,

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

Goal state before:
pp: case refine_2
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₂ ∘ₖ Kernel.id.map f₁ = Kernel.id

Tactic:
Kernel.deterministic_comp_eq_map hf₂,

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
⊢ Z ⟂ᵢ[P] U

Tactic:
indepFun_iff_map_prod_eq_prod_map_map mZ mU

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
⊢ map (fun ω ↦ (Z ω, U ω)) P = (map Z P).prod (map U P)
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndepSet m' hm' s μ ↔ iCondIndep m' hm' (fun i ↦ generateFrom {s i}) μ

Tactic:
simp only [iCondIndepSet, iCondIndep, Kernel.iIndepSet]

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

Goal state before:
pp: Y : Type u_2
inst✝² : Nonempty Y
mY : MeasurableSpace Y
inst✝¹ : StandardBorelSpace Y
μ : Measure Y
inst✝ : IsProbabilityMeasure μ
f : Unit → ↑I → Y
hf_meas : Measurable (uncurry f)
hf_map : ∀ (a : Unit), map (f a) volume = (Kernel.const Unit μ) a
⊢ ∃ f, Measurable f ∧ map f volume = μ

Tactic:
specialize hf_map ()

Goal state after:
Y : Type u_2
inst✝² : Nonempty Y
mY : MeasurableSpace Y
inst✝¹ : StandardBorelSpace Y
μ : Measure Y
inst✝ : IsProbabilityMeasure μ
f : Unit → ↑I → Y
hf_meas : Measurable (uncurry f)
hf_map : map (f ()) volume = (Kernel.const Unit μ) ()
⊢ ∃ f, Measurable f ∧ map f volume = μ
Module: Mathlib.Probability.Moments.Tilted

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

Tactic:
rcases eq_zero_or_neZero μ with rfl | hμ
  · simp
  · simp_rw [setIntegral_tilted_mul_eq_mgf' _ hs, exp_sub, exp_cgf ht]

Goal state after:
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 : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : 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))

Tactic:
hpX

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 : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : 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))
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case succ.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 : ℕ
a✝ :
  ((∀ 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) μ) →
    (∀ 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) μ
hn : HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
h_subG : ∀ i < n + 1 + 1 - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
m : ℕ
hm : m ∈ Finset.range (n + 1)
⊢ m ≤ n

Tactic:
simp only [Finset.mem_range] at hm

Goal state after:
case succ.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 : ℕ
a✝ :
  ((∀ 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) μ) →
    (∀ 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) μ
hn : HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
h_subG : ∀ i < n + 1 + 1 - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
m : ℕ
hm : m < n + 1
⊢ m ≤ n
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : 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 ω) =o[atTop] fun n ↦ ↑n

Tactic:
convert! isLittleO_sum_range_of_tendsto_zero hω using 1

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)
⊢ (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 ω)