mathlib-initiative/mathlib-tactics huggingface dataset:
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)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (f n) ↑(Iic (a n))
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto : ∀ (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X ↑i
hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (f n) (updateFinset x (Iic k) y)
x✝ : ∀ (n : ℕ), Nonempty (X n)
F : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (l x))
f_eq : ∀ (x : (n : ℕ) → X n) (n : ℕ), lmarginalPartialTraj κ k (a n) (f n) x = lmarginalPartialTraj κ k (k + 1) (F n) x
F_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), F n x ≤ bound
x : (n : ℕ) → X n
⊢ Tendsto
    (fun n ↦
      ∫⁻ (z : (i : ↥(Iic (k + 1))) → X ↑i),
        F n (updateFinset x (Iic (k + 1)) z) ∂(partialTraj κ k (k + 1)) (frestrictLe k x))
    atTop
    (𝓝
      (∫⁻ (z : (i : ↥(Iic (k + 1))) → X ↑i),
        l (updateFinset x (Iic (k + 1)) z) ∂(partialTraj κ k (k + 1)) (frestrictLe k x)))

Tactic:
exact tendsto_lintegral_of_dominated_convergence (fun _ ↦ bound)
      (fun n ↦ (measurable_lmarginalPartialTraj _ _ (mf n)).comp measurable_updateFinset)
      (fun n ↦ Eventually.of_forall <| fun y ↦ F_le n _)
      (by simp [fin_bound]) (Eventually.of_forall (fun _ ↦ tendstoF _))

Goal state after:
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 : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) -
      ENNReal.ofReal ((1 - κ.rnDerivAux (κ + η) a x) * ((1 - κ.rnDerivAux (κ + η) a x)⁻¹ * κ.rnDerivAux (κ + η) a x)) =
    0 x

pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 ≤ 1 - κ.rnDerivAux (κ + η) a x

pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 < 1 - κ.rnDerivAux (κ + η) a x

Tactic:
← mul_assoc,

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) -
      ENNReal.ofReal ((1 - κ.rnDerivAux (κ + η) a x) * (1 - κ.rnDerivAux (κ + η) a x)⁻¹ * κ.rnDerivAux (κ + η) a x) =
    0 x

α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 ≤ 1 - κ.rnDerivAux (κ + η) a x

α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 < 1 - κ.rnDerivAux (κ + η) a x
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 : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 < 1 - κ.rnDerivAux (κ + η) a x

Tactic:
simp only [sub_pos, hx]

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

Goal state before:
pp: case refine_1
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn f ↑(Iic a)
hab : a ≤ b
x : (n : ℕ) → X n
⊢ IsProbabilityMeasure (((partialTraj κ b c).map (restrict₂ ⋯)) (frestrictLe b x))

pp: case refine_2
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn f ↑(Iic a)
hab : a ≤ b
x : (n : ℕ) → X n
y : (i : ↥(Ioc b c)) → X ↑i
i : ℕ
hi : i ∈ ↑(Iic a)
⊢ Function.updateFinset x (Ioc b c) y i = x i

Tactic:
· refine @IsMarkovKernel.isProbabilityMeasure _ _ _ _ _ ?_ _
    exact IsMarkovKernel.map _ (by fun_prop)

Goal state after:
case refine_2
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn f ↑(Iic a)
hab : a ≤ b
x : (n : ℕ) → X n
y : (i : ↥(Ioc b c)) → X ↑i
i : ℕ
hi : i ∈ ↑(Iic a)
⊢ Function.updateFinset x (Ioc b c) y i = x i
Module: Mathlib.Probability.Kernel.CompProdEqIff

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

Tactic:
have hκ_eq : ∀ᵐ a ∂μ, κ a = η.withDensity (κ.rnDeriv η) a := by
    filter_upwards [h_ac] with a ha using (Kernel.withDensity_rnDeriv_eq ha).symm

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

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

Tactic:
by
    filter_upwards [h_ac, this] with a h_ac h using (rnDeriv_eq_one_iff_eq h_ac).mp h

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Finset ι
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
this : (↑s).pi t = cylinder s (Set.univ.pi fun i ↦ t ↑i)
⊢ Measurable s.restrict

Tactic:
exact measurable_restrict _

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
s' : Finset ↑s
| (infinitePi μ) (s.domRestrict ⁻¹' (↑s').pi fun i ↦ t ↑i)

Tactic:
domRestrict_preimage

Goal state after:
ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
s' : Finset ↑s
| (infinitePi μ) ((↑(image Subtype.val s')).pi fun i ↦ if h : i ∈ s then t ↑⟨i, h⟩ else Set.univ)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case cylinder
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
ht : t ∈ measurableCylinders X
N : ℕ
S : Set ((i : ↥(Iic N)) → X ↑i)
mS : MeasurableSet S
t_eq : t = cylinder (Iic N) S
⊢ Measurable fun x₀ ↦ Measure.map (restrict₂ ⋯) ((partialTraj κ a ((Iic N).sup id)) x₀)

Tactic:
exact (Measure.measurable_map _ (measurable_restrict₂ _)).comp (measurable _)

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Countable ι
t : (i : ι) → Set (X i)
mt : ∀ (i : ι), MeasurableSet (t i)
⊢ (infinitePi μ) (Set.univ.pi t) = ∏' (i : ι), (μ i) (t i)

Tactic:
rw [infinitePi_pi_of_countable, tprod_univ (f := fun i ↦ μ i (t i))]

Goal state after:
case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Countable ι
t : (i : ι) → Set (X i)
mt : ∀ (i : ι), MeasurableSet (t i)
⊢ Countable ↑Set.univ

case mt
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Countable ι
t : (i : ι) → Set (X i)
mt : ∀ (i : ι), MeasurableSet (t i)
⊢ ∀ i ∈ Set.univ, MeasurableSet (t i)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ map (⇑(MeasurableEquiv.curry ι κ X).symm) (infinitePi fun i ↦ infinitePi fun j ↦ μ i j) = infinitePi fun p ↦ μ p.1 p.2

Tactic:
by
  rw [← (MeasurableEquiv.piCongrLeft (fun _ ↦ X)
    (Equiv.sigmaEquivProd ι κ).symm).map_measurableEquiv_injective.eq_iff, map_map]
  · have : (MeasurableEquiv.piCongrLeft (fun _ ↦ X) (Equiv.sigmaEquivProd ι κ).symm) ∘
        (MeasurableEquiv.curry ι κ X).symm = ⇑(MeasurableEquiv.piCurry (fun _ _ ↦ X)).symm := by
      ext; simp [piCongrLeft, Equiv.piCongrLeft, Sigma.uncurry]
    rw [this, infinitePi_map_piCurry_symm]
    convert! infinitePi_map_piCongrLeft (fun p ↦ μ p.1 p.2) (Equiv.sigmaEquivProd ι κ).symm |>.symm
  all_goals fun_prop

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : AEMeasurable f ((traj κ a) x₀)
⊢ ∫⁻ (x : (n : ℕ) → X n), f x ∂(traj κ a) x₀ = ∫⁻ (x : (n : ℕ) → X n), f (updateFinset x (Iic a) x₀) ∂(traj κ a) x₀

Tactic:
by
  nth_rw 1 [← traj_map_updateFinset, MeasureTheory.lintegral_map']
  · convert! mf
    exact traj_map_updateFinset x₀
  · exact measurable_updateFinset_left.aemeasurable

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)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) x₀ ⊗ₘ traj κ b)
hf' : Integrable (uncurry f) (Measure.map (fun x ↦ (frestrictLe b x, x)) ((traj κ a) x₀))
⊢ ∫ (x : ((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n)),
      uncurry f x ∂Measure.map (fun x ↦ (frestrictLe b x, x)) ((traj κ a) x₀) =
    ∫ (x : (n : ℕ) → X n), uncurry f (frestrictLe b x, x) ∂(traj κ a) x₀

Tactic:
integral_map (by fun_prop) hf'.1

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

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ r ^ a * ((1 / r) ^ a * Gamma a) / Gamma a = 1

Tactic:
← mul_assoc,

Goal state after:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ r ^ a * (1 / r) ^ a * Gamma a / Gamma a = 1
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
p : PMF α
s : Set α
⊢ ∑' (x : α), s.indicator (⇑p) x = 0 ↔ Disjoint p.support s

Tactic:
ENNReal.tsum_eq_zero

Goal state after:
α : Type u_1
p : PMF α
s : Set α
⊢ (∀ (i : α), s.indicator (⇑p) i = 0) ↔ Disjoint p.support s
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ (gammaMeasure a r) univ = 1

Tactic:
simp [gammaMeasure, lintegral_gammaPDF_eq_one ha hr]

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

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

Tactic:
refine _root_.trans ENNReal.tsum_comm (tsum_congr fun b => tsum_congr fun a => ?_)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
b : β
a : α
⊢ (p a * if h : p a = 0 then 0 else q b * if h : q b = 0 then 0 else (f a h b h) c) =
    q b * if h : q b = 0 then 0 else p a * if h : p a = 0 then 0 else (f a h b h) c
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : IsUniform X s ℙ volume
⊢ ∫ (x : Ω), X x ∂ℙ = (volume s)⁻¹.toReal • ∫ (x : ℝ) in s, x

Tactic:
← integral_smul_measure

Goal state after:
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : IsUniform X s ℙ volume
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂(volume s)⁻¹ • volume.restrict s
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂(volume s)⁻¹ • volume.restrict s

Tactic:
rw [← huX]

Goal state after:
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂Measure.map X ℙ
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
this : IsFiniteMeasure ν
⊢ (Measure.map Z ν).prod (Measure.map Y μ) = (Measure.map Z ν).prod (Measure.map W ν)

Tactic:
hYW.map_eq

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 ν).prod (Measure.map W ν) = (Measure.map Z ν).prod (Measure.map W ν)
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: ι : Type u_1
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), Measurable (X i)
i : ι
⊢ map (X i) (P i) = map (fun ω ↦ X i (ω i)) (infinitePi P)

Tactic:
rw [← infinitePi_map_eval P i, map_map (mX i) (by fun_prop), Function.comp_def]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ (ofMultiset s hs).toOuterMeasure t =
    (∑' (x : α), ↑(Multiset.count x (Multiset.filter (fun x ↦ x ∈ t) s))) * (↑s.card)⁻¹

Tactic:
← ENNReal.tsum_mul_right,

Goal state after:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ (ofMultiset s hs).toOuterMeasure t = ∑' (i : α), ↑(Multiset.count i (Multiset.filter (fun x ↦ x ∈ t) s)) * (↑s.card)⁻¹
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: case refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (t : Set ι), BddAbove t → tᶜ ∈ atTop

Tactic:
simp only [mem_atTop_sets, Set.mem_compl_iff, BddAbove, upperBounds, Set.Nonempty]

Goal state after:
case refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
⊢ ∀ (t : Set ι), (∃ x, x ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}) → ∃ a, ∀ (b : ι), a ≤ b → b ∉ t
Module: Mathlib.Probability.Kernel.Proper

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

Tactic:
simp [isProper_iff_restrict_eq_indicator_smul h𝓑𝓧, Measure.ext_iff]

Goal state after:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ (∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X) (s : Set X),
      MeasurableSet s → ((π.restrict ⋯) x) s = B.indicator (fun x ↦ 1) x * (π x) s) ↔
    ∀ ⦃A : Set X⦄,
      MeasurableSet A → ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), ((π.restrict ⋯) x) A = B.indicator 1 x * (π x) A
Module: Mathlib.Probability.Kernel.Proper

Goal state before:

Tactic:
_ ↔ ∀ ⦃A : Set X⦄ (_hA : MeasurableSet[𝓧] A) ⦃B : Set X⦄ (hB : MeasurableSet[𝓑] B) (x : X),
          π.restrict (h𝓑𝓧 _ hB) x A = B.indicator 1 x * π x A := by
      simp [isProper_iff_restrict_eq_indicator_smul h𝓑𝓧, Measure.ext_iff]; aesop
    _ ↔ _ := by congr! 5 with A hA B hB x; rw [restrict_apply, Measure.restrict_apply hA]

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

Goal state before:
pp: X Y Z : SFinKer
κ : Y ⟶ Z
⊢ Kernel.swap X.carrier Z.carrier ∘ₖ (Kernel.id ∥ₖ κ.hom) = κ.hom ∥ₖ Kernel.id ∘ₖ Kernel.swap X.carrier Y.carrier

Tactic:
exact Kernel.swap_parallelComp

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

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
X : SFinKer
⊢ Kernel.swap Y✝.carrier X.carrier ∘ₖ (κ.hom ∥ₖ Kernel.id) = Kernel.id ∥ₖ κ.hom ∘ₖ Kernel.swap X✝.carrier X.carrier

Tactic:
exact Kernel.swap_parallelComp

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 Y : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
h : ∀ (t : T), X t =ᵐ[P] Y t
t : T
⊢ Y t =ᵐ[P] IsAEKolmogorovProcess.mk X hX t

Tactic:
filter_upwards [hX.ae_eq_mk t, h t] with ω hX hY using hY.symm.trans hX

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
𝓕 : Filtration ι mΩ
P : Measure Ω
n : ℕ
⊢ IsStoppingTime 𝓕 fun x ↦ ⊤

Tactic:
simp [IsStoppingTime]

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

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

Tactic:
simp only [Submodule.mem_inf, and_imp]
      rintro g x hx₁ hx₂
      exact ⟨ρ₁.apply_mem_toSubmodule g hx₁, ρ₂.apply_mem_toSubmodule g hx₂⟩

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
N : Submodule A[G] ρ.asModule
a : A
w : W
hw : w ∈ N.carrier
⊢ a • w ∈ N.carrier

Tactic:
simpa using! (N.smul_mem (algebraMap A A[G] a) hw)

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ Integrable (truncation f A) μ

Tactic:
← memLp_one_iff_integrable

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ MemLp (truncation f A) 1 μ
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : α) ∂μ, ‖truncation f n a‖ ≤ |f a|

pp: case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (fun x ↦ |f x|) μ

pp: case refine_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ truncation f n a) atTop (𝓝 (f a))

Tactic:
· filter_upwards with A
    filter_upwards with x
    rw [Real.norm_eq_abs]
    exact abs_truncation_le_abs_self _ _ _

Goal state after:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (fun x ↦ |f x|) μ

case refine_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ truncation f n a) atTop (𝓝 (f a))