mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) := {s | ∃ t ∈ squareCylinders fun i ↦ {s | MeasurableSet s}, (fun ω i ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
πX_gen : MeasurableSpace.comap (fun ω i ↦ X i ω) MeasurableSpace.pi = generateFrom πX
I : Finset S
s : (i : S) → Set (𝓧 i)
t : Set 𝓨
ht : MeasurableSet t
hs : ∀ (i : S), MeasurableSet (s i)
this : (fun ω i ↦ X i ω) ⁻¹' (↑I).pi s = (fun ω i ↦ X (↑i) ω) ⁻¹' (↑Finset.univ).pi fun i ↦ s ↑i
h1 : MeasurableSet ((↑Finset.univ).pi fun i ↦ s ↑i)
⊢ ∀ᵐ (a : α) ∂P,
    (κ a) ((fun ω i ↦ X i ω) ⁻¹' (↑I).pi s ∩ Y ⁻¹' t) = (κ a) ((fun ω i ↦ X i ω) ⁻¹' (↑I).pi s) * (κ a) (Y ⁻¹' t)

Tactic:
filter_upwards [(h I).measure_inter_preimage_eq_mul _ _ h1 ht] with ω hω

Goal state after:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) := {s | ∃ t ∈ squareCylinders fun i ↦ {s | MeasurableSet s}, (fun ω i ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
πX_gen : MeasurableSpace.comap (fun ω i ↦ X i ω) MeasurableSpace.pi = generateFrom πX
I : Finset S
s : (i : S) → Set (𝓧 i)
t : Set 𝓨
ht : MeasurableSet t
hs : ∀ (i : S), MeasurableSet (s i)
this : (fun ω i ↦ X i ω) ⁻¹' (↑I).pi s = (fun ω i ↦ X (↑i) ω) ⁻¹' (↑Finset.univ).pi fun i ↦ s ↑i
h1 : MeasurableSet ((↑Finset.univ).pi fun i ↦ s ↑i)
ω : α
hω :
  (κ ω) (((fun ω i ↦ X (↑i) ω) ⁻¹' (↑Finset.univ).pi fun i ↦ s ↑i) ∩ Y ⁻¹' t) =
    (κ ω) ((fun ω i ↦ X (↑i) ω) ⁻¹' (↑Finset.univ).pi fun i ↦ s ↑i) * (κ ω) (Y ⁻¹' t)
⊢ (κ ω) ((fun ω i ↦ X i ω) ⁻¹' (↑I).pi s ∩ Y ⁻¹' t) = (κ ω) ((fun ω i ↦ X i ω) ⁻¹' (↑I).pi s) * (κ ω) (Y ⁻¹' t)
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:

Tactic:
μ {x | ‖x‖ ≤ a}
        _ ≤ μ {x | ‖x‖ ≤ 1} := measure_mono fun x hx ↦ hx.trans (ha.trans (by positivity))
        _ ≤ 2⁻¹ := h_of_pos _ (by positivity)

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

Goal state before:
pp: case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
⊢ IsGaussianProcess (fun t ω ↦ (√↑c)⁻¹ * B (c * t) ω) P

Tactic:
have this t ω : (√c)⁻¹ * B (c * t) ω = (√c)⁻¹ • ((B ∘ (c * ·)) t ω) := rfl

Goal state after:
case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
this : ∀ (t : ℝ≥0) (ω : Ω), (√↑c)⁻¹ * B (c * t) ω = (√↑c)⁻¹ • (B ∘ fun x ↦ c * x) t ω
⊢ IsGaussianProcess (fun t ω ↦ (√↑c)⁻¹ * B (c * t) ω) P
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: case refine_1
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun n ↦ Iic ↑(s n)
i j : ℕ
hij : i ≤ j
⊢ ↑(s j) ≤ ↑(s i)

Tactic:
exact mod_cast hs_anti hij

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ✝ : Kernel α (β × Ω)
κCond✝ : Kernel (α × β) Ω
inst✝³ : Countable α
κCond : α → Kernel β Ω
inst✝² : ∀ (a : α), IsMarkovKernel (κCond a)
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
inst✝ : ∀ (a : α), (κ a).IsCondKernel (κCond a)
⊢ κ.IsCondKernel (condKernelCountable κCond h_atom)

Tactic:
by
  constructor
  ext a s hs
  conv_rhs => rw [← (κ a).disintegrate (κCond a)]
  simp_rw [compProd_apply hs, condKernelCountable_apply, Measure.compProd_apply hs]
  congr

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ∫⁻ (x : β), (κ.condKernel (a, x)) (Prod.mk x ⁻¹' s) ∂κ.fst a = ((κ.fst ⊗ₖ κ.condKernel) a) s

Tactic:
simp_rw [Kernel.compProd_apply hs]

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

Goal state before:
pp: α : Type u_1
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
Y : α → Ω
⊢ ⇑(condDistrib Y Y μ) =ᵐ[Measure.map Y μ] ⇑Kernel.id

Tactic:
simpa using! condDistrib_comp_self Y measurable_id

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

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
a : ℕ
⊢ partialTraj κ a (a + 1) = (Kernel.id ×ₖ (κ a).map ⇑(piSingleton a)).map (_root_.IicProdIoc a (a + 1))

Tactic:
rw [partialTraj_succ_of_le le_rfl, partialTraj_self, comp_id]

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
h : ∀ᵐ (a_1 : γ) ∂κ.fst a, ∀ (i : ℕ), κ.densityProcess κ.fst i a a_1 univ = 1
⊢ ∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x univ = 1

Tactic:
filter_upwards [h] with x hx

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
h : ∀ᵐ (a_1 : γ) ∂κ.fst a, ∀ (i : ℕ), κ.densityProcess κ.fst i a a_1 univ = 1
x : γ
hx : ∀ (i : ℕ), κ.densityProcess κ.fst i a x univ = 1
⊢ κ.density κ.fst a x univ = 1
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : 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
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
this : min (f a b) (↑n + 1) = f a b ∧ min (f a b) ↑n = f a b
⊢ fs n a b = 0

Tactic:
fs,

Goal state after:
α : 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
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
this : min (f a b) (↑n + 1) = f a b ∧ min (f a b) ↑n = f a b
⊢ min (f a b) (↑n + 1) - min (f a b) ↑n = 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 n : ℕ
η : Kernel ((i : ↥(Iic a)) → X ↑i) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe b) = partialTraj κ a b
⊢ η = traj κ a

Tactic:
ext x : 1

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 n : ℕ
η : Kernel ((i : ↥(Iic a)) → X ↑i) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe b) = partialTraj κ a b
x : (i : ↥(Iic a)) → X ↑i
⊢ η x = (traj κ a) x
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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ (map (⇑(piCongrLeft X e)) (infinitePi fun i ↦ μ (e i))) ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)

Tactic:
conv_lhs => enter [2, 1]; rw [← e.image_preimage s, ← coe_preimage _ e.injective.injOn]

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ (map (⇑(piCongrLeft X e)) (infinitePi fun i ↦ μ (e i))) ((⇑e '' ↑(s.preimage ⇑e ⋯)).pi t) = ∏ i ∈ s, (μ i) (t i)
Module: Mathlib.Probability.Distributions.Beta

Goal state before:
pp: α β : ℝ
⊢ ∫⁻ (x : ℝ) in Iio 1 ∩ Ioi 0, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))

Tactic:
Iio_inter_Ioi,

Goal state after:
α β : ℝ
⊢ ∫⁻ (x : ℝ) in Ioo 0 1, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
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 : ℕ
hab : a ≤ b
x₀ : (n : ↥(Iic a)) → X ↑n
hf : (fun x ↦ (frestrictLe b x, x (b + 1))) = (Prod.map id fun x ↦ x (b + 1)) ∘ fun x ↦ (frestrictLe b x, x)
⊢ (partialTraj κ a b) x₀ ⊗ₘ κ b = (partialTraj κ a b) x₀ ⊗ₘ (traj κ b).map fun x ↦ x (b + 1)

Tactic:
map_traj_succ_self

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 : ℕ
hab : a ≤ b
x₀ : (n : ↥(Iic a)) → X ↑n
hf : (fun x ↦ (frestrictLe b x, x (b + 1))) = (Prod.map id fun x ↦ x (b + 1)) ∘ fun x ↦ (frestrictLe b x, x)
⊢ (partialTraj κ a b) x₀ ⊗ₘ κ b = (partialTraj κ a b) x₀ ⊗ₘ κ b
Module: Mathlib.Probability.Distributions.Gamma

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

Tactic:
lintegral_union measurableSet_Icc

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

y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
⊢ Disjoint (Iio z) (Icc z y)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝³ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝² : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ ∫ (x : (i : ↥(Iic b)) → X ↑i) in A, ∫ (y : (n : ℕ) → X n), f x y ∂(traj κ b) x ∂(partialTraj κ a b) u =
    ∫ (y : (n : ℕ) → X n) in frestrictLe b ⁻¹' A, f (frestrictLe b y) y ∂(traj κ a) u

Tactic:
rw [← integral_integral_indicator _ _ _ hA, integral_traj_partialTraj' hab]

Goal state after:
X : ℕ → Type u_1
inst✝³ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝² : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ ∫ (x : (n : ℕ) → X n), A.indicator (fun x_1 ↦ f x_1 x) (frestrictLe b x) ∂(traj κ a) u =
    ∫ (y : (n : ℕ) → X n) in frestrictLe b ⁻¹' A, f (frestrictLe b y) y ∂(traj κ a) u

X : ℕ → Type u_1
inst✝³ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝² : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ Integrable (uncurry fun x y ↦ A.indicator (fun x ↦ f x y) x) ((partialTraj κ a b) u ⊗ₘ traj κ b)
Module: Mathlib.Probability.IdentDistribIndep

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst✝ : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
⊢ IsFiniteMeasure ν

Tactic:
have : IsFiniteMeasure (ν.map Z) := by rw [← hXZ.map_eq]; infer_instance

Goal state after:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst✝ : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
this : IsFiniteMeasure (Measure.map Z ν)
⊢ IsFiniteMeasure ν
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: α : Type u_1
s : Multiset α
hs : s ≠ 0
a : α
ha : a ∉ s.toFinset
⊢ a ∉ s

Tactic:
← Multiset.mem_toFinset

Goal state after:
α : Type u_1
s : Multiset α
hs : s ≠ 0
a : α
ha : a ∉ s.toFinset
⊢ a ∉ s.toFinset
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ}, MeasurableSet s → MeasurableSet (k ⁻¹' s)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ μ ((fun ω ↦ (k ω, f ω, g ω)) ⁻¹' s ×ˢ t ×ˢ u) = μ ((fun ω ↦ (ω, f ω, g ω)) ⁻¹' (k ⁻¹' s) ×ˢ t ×ˢ u)

pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ}, MeasurableSet s → MeasurableSet (k ⁻¹' s)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ Measurable fun ω ↦ (ω, f ω, g ω)

Tactic:
· simp [Set.mk_preimage_prod]

Goal state after:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ}, MeasurableSet s → MeasurableSet (k ⁻¹' s)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ Measurable fun ω ↦ (ω, f ω, g ω)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
κ : Kernel X.carrier Y.carrier
inst✝¹ : IsDeterministic κ
inst✝ : IsMarkovKernel κ
⊢ Kernel.copy Y.carrier ∘ₖ κ = Kernel.id ∥ₖ κ ∘ₖ (κ ∥ₖ Kernel.id) ∘ₖ Kernel.copy X.carrier

Tactic:
Kernel.id_parallelComp_comp_parallelComp_id

Goal state after:
X Y : SFinKer
κ : Kernel X.carrier Y.carrier
inst✝¹ : IsDeterministic κ
inst✝ : IsMarkovKernel κ
⊢ Kernel.copy Y.carrier ∘ₖ κ = κ ∥ₖ κ ∘ₖ Kernel.copy X.carrier
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: case refine_1
Ω : 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✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ ↑i
h_int : Integrable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ)) μ
t : Set Ω
ht : MeasurableSet (t ∩ {ω | τ ω ≤ σ ω})
⊢ MeasurableSet (t ∩ {ω | τ ω ≤ σ ω})

Tactic:
IsStoppingTime.measurableSet_min_iff hτ hσ

Goal state after:
case refine_1
Ω : 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✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ ↑i
h_int : Integrable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ)) μ
t : Set Ω
ht : MeasurableSet (t ∩ {ω | τ ω ≤ σ ω}) ∧ MeasurableSet (t ∩ {ω | τ ω ≤ σ ω})
⊢ MeasurableSet (t ∩ {ω | τ ω ≤ σ ω})
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:
by
  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.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
⊢ ∫⁻ (a : Ω), edist (X s a) (X t a) ^ p ∂P ≤ 0

Tactic:
calc ∫⁻ ω, edist (X s ω) (X t ω) ^ p ∂P
  _ ≤ M * edist s t ^ q := hX.kolmogorovCondition s t
  _ = 0 := by simp [h, hX.q_pos]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ ∫ (y : ℝ), (Set.Ioc (-A) A).indicator id y ^ n ∂Measure.map f μ =
    ∫ (x : ℝ), (Set.Ioc (-A) A).indicator (fun x ↦ x ^ n) x ∂Measure.map f μ

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ -A ≤ A

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ AEStronglyMeasurable (fun z ↦ (Set.Ioc (-A) A).indicator id z ^ n) (Measure.map f μ)

Tactic:
· simp only [indicator, zero_pow hn, id, ite_pow]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ -A ≤ A

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ AEStronglyMeasurable (fun z ↦ (Set.Ioc (-A) A).indicator id z ^ n) (Measure.map f μ)
Module: Mathlib.Probability.StrongLaw

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

pp: case inl
α : 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 : 0 ≤ A
⊢ AEStronglyMeasurable (fun z ↦ (Set.Ioc 0 A).indicator id z ^ n) (Measure.map f μ)

Tactic:
· simp only [indicator, zero_pow hn, id, ite_pow]

Goal state after:
case inl
α : 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 : 0 ≤ A
⊢ AEStronglyMeasurable (fun z ↦ (Set.Ioc 0 A).indicator id z ^ n) (Measure.map f μ)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case 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 η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
hX_int : Integrable (fun y ↦ rexp (↑q * X y)) (κ ω')
hY_mgf : ∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)
h_int_mul : Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω')
⊢ (fun x ↦ rexp (↑q * X x) * ∫ (y : Ω''), rexp (↑q * Y y) ∂η (ω', x)) ≤ᵐ[κ ω'] fun x ↦
    rexp (↑q * X x) * rexp (↑cY * ↑q ^ 2 / 2)

Tactic:
filter_upwards [all_ae_of hY_mgf q] with ω hY_mgf

Goal state after:
Ω : 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 η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
hX_int : Integrable (fun y ↦ rexp (↑q * X y)) (κ ω')
hY_mgf✝ : ∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)
h_int_mul : Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω')
ω : Ω
hY_mgf : mgf Y (η (ω', ω)) ↑q ≤ rexp (↑cY * ↑q ^ 2 / 2)
⊢ rexp (↑q * X ω) * ∫ (y : Ω''), rexp (↑q * Y y) ∂η (ω', ω) ≤ rexp (↑q * X ω) * rexp (↑cY * ↑q ^ 2 / 2)
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 ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∑ k ∈ range K, (∑ j ∈ Ioo k K, (↑j ^ 2)⁻¹) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ ≤
    ∑ k ∈ range K, 2 / (↑k + 1) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ

Tactic:
gcongr with k
      · refine intervalIntegral.integral_nonneg_of_forall ?_ fun u => sq_nonneg _
        simp
      · apply sum_Ioo_inv_sq_le

Goal state after: