mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
h' : IsGaussian μ
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ

Tactic:
simp_rw [h'.charFunDual_eq', Complex.exp_eq_exp_iff_exists_int] at h

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
h :
  ∀ (L : StrongDual ℝ E),
    ∃ n,
      ↑(L (∫ (x : E), id x ∂μ)) * I - ↑(((covarianceBilinDual μ) L) L) / 2 =
        ↑(L m) * I - ↑((f L) L) / 2 + ↑n * (2 * ↑π * I)
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝³ : NormedSpace ℝ E
inst✝² : BorelSpace E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ((covarianceBilinDual μ) L₁) L₂ = ∫ (x : E), L₁ (x - ∫ (x : E), id x ∂μ) * L₂ (x - ∫ (x : E), id x ∂μ) ∂μ

Tactic:
covarianceBilinDual_apply h

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝³ : NormedSpace ℝ E
inst✝² : BorelSpace E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ∫ (x : E), (L₁ x - ∫ (x : E), L₁ x ∂μ) * (L₂ x - ∫ (x : E), L₂ x ∂μ) ∂μ =
    ∫ (x : E), L₁ (x - ∫ (x : E), id x ∂μ) * L₂ (x - ∫ (x : E), id x ∂μ) ∂μ
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
X : Ω → E
inst✝² : NormedSpace ℝ E
inst✝¹ : Subsingleton E
inst✝ : IsProbabilityMeasure P
⊢ IsGaussian (Measure.map X P)

Tactic:
have : IsProbabilityMeasure (P.map X) := P.isProbabilityMeasure_map (by fun_prop)
    exact .of_subsingleton

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
X : Ω → E
inst✝ : InnerProductSpace ℝ E
t : E
hX : HasGaussianLaw X P
⊢ cexp ((∫ (x : E), ↑((fun x ↦ ⟪t, x⟫) x) ∂Measure.map X P) * I - ↑Var[fun x ↦ ⟪t, x⟫; Measure.map X P] / 2) =
    cexp (↑(∫ (x : Ω), (fun ω ↦ ⟪t, X ω⟫) x ∂P) * I - ↑Var[fun ω ↦ ⟪t, X ω⟫; P] / 2)

Tactic:
integral_map hX.aemeasurable (by fun_prop),

Goal state after:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
X : Ω → E
inst✝ : InnerProductSpace ℝ E
t : E
hX : HasGaussianLaw X P
⊢ cexp ((∫ (x : Ω), ↑((fun x ↦ ⟪t, x⟫) (X x)) ∂P) * I - ↑Var[fun x ↦ ⟪t, x⟫; Measure.map X P] / 2) =
    cexp (↑(∫ (x : Ω), (fun ω ↦ ⟪t, X ω⟫) x ∂P) * I - ↑Var[fun ω ↦ ⟪t, X ω⟫; P] / 2)
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
X : Ω → E
inst✝ : NormedSpace ℝ E
L : StrongDual ℝ E
hX : HasGaussianLaw X P
⊢ cexp ((∫ (x : E), ↑(L x) ∂Measure.map X P) * I - ↑Var[⇑L; Measure.map X P] / 2) =
    cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2)

Tactic:
integral_map hX.aemeasurable (by fun_prop),

Goal state after:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
X : Ω → E
inst✝ : NormedSpace ℝ E
L : StrongDual ℝ E
hX : HasGaussianLaw X P
⊢ cexp ((∫ (x : Ω), ↑(L (X x)) ∂P) * I - ↑Var[⇑L; Measure.map X P] / 2) =
    cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2)
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess

Goal state before:
pp: T : Type u_1
inst✝¹ : LinearOrder T
I : Finset T
inst✝ : Bot T
i : Fin (#I + 1)
hi : i ≠ 0
⊢ I.orderEmbOfFinWithBot i = (I.orderEmbOfFin ⋯) (i.pred hi)

Tactic:
rw [orderEmbOfFinWithBot, dif_neg hi]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun r ↦ (ρ.IicSnd ↑r) s) atBot (𝓝 0)

Tactic:
ρ.IicSnd_apply _ hs

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑r)) atBot (𝓝 0)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
⊢ ∀ᵐ (c : β) ∂ν a, Monotone (f (a, c))

Tactic:
by
  unfold Monotone
  simp_rw [ae_all_iff]
  exact fun _ _ hqr ↦ hf.mono' a hqr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
⊢ ∫ (b : β), ↑(f (a, b)) x ∂ν a = (κ a).real (univ ×ˢ Iic x)

Tactic:
by
  rw [← hf.setIntegral _ MeasurableSet.univ, Measure.restrict_univ]

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

Goal state before:
pp: case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
⊢ ∀ (s : ℝ≥0) (t : ↑(Set.Iic t₀)), cov[fun ω ↦ B (t₀ + s) ω - B t₀ ω, B ↑t; P] = 0

Tactic:
rintro s ⟨t, ht : t ≤ t₀⟩
    have := hB.isGaussianProcess.isProbabilityMeasure
    rw [covariance_fun_sub_left, hB.covariance_eval, hB.covariance_eval, min_eq_right, min_eq_right,
      sub_self]
    · grind
    · simp [ht, le_add_right]
    all_goals exact (hB.isGaussianProcess.hasGaussianLaw_eval _).memLp_two

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
⊢ ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P

Tactic:
refine ae_all_iff.2 fun n ↦ ?_

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
n : ℕ
⊢ ∀ᵐ (a : Ω) ∂P, X n a = ∫ (x : Ω), X 0 x ∂P
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) univ ∂ν a -
      ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a =
    (κ a) (s ×ˢ univ) - (κ a) (s ×ˢ t)

Tactic:
rw [setLIntegral_toKernel_univ hf a hs, iht]

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

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst✝² : Nonempty Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
s : Set Ω
hs : MeasurableSet s
he : MeasurableEmbedding (embeddingReal Ω)
h : ¬(η a) (range (embeddingReal Ω))ᶜ = 0
⊢ (Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose ⋯))) s =
    (embeddingReal Ω '' s).indicator 1 (Exists.choose ⋯)

Tactic:
rw [Measure.comap_apply _ he.injective he.measurableSet_image' _ hs, Measure.dirac_apply]

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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ κ.densityProcess ν n a x s ≤ κ.densityProcess ν n a x s'

Tactic:
by
  unfold densityProcess
  obtain h₀ | h₀ := eq_or_ne (ν a (countablePartitionSet n x)) 0
  · simp [h₀]
  · gcongr
    simp only [ne_eq, ENNReal.div_eq_top, h₀, and_false, false_or, not_and, not_not]
    exact eq_top_mono (meas_countablePartitionSet_le_of_fst_le hκν n a x s')

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd : (κ' a) (univ ×ˢ range e)ᶜ = 0
⊢ ∀ᵐ (t : β) ∂κ'.fst a, (a, t) ∈ {p | (η p) (range e)ᶜ = 0}

Tactic:
rw [← hη', compProd_null] at h_compProd

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd : (fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' (univ ×ˢ range e)ᶜ)) =ᵐ[κ'.fst a] 0
⊢ ∀ᵐ (t : β) ∂κ'.fst a, (a, t) ∈ {p | (η p) (range e)ᶜ = 0}

case hs
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd : ((κ'.fst ⊗ₖ η) a) (univ ×ˢ range e)ᶜ = 0
⊢ MeasurableSet (univ ×ˢ range e)ᶜ
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case hm
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ Antitone fun m ↦ countablePartitionSet n x ×ˢ seq m

Tactic:
exact fun _ _ h ↦ prod_mono_right <| hseq h

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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
⊢ ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)

Tactic:
suffices ∫ x in A, density κ ν a x s ∂(ν a) = ∫ x in A, densityProcess κ ν n a x s ∂(ν a) by
    exact this ▸ setIntegral_densityProcess hκν _ _ hs hA
  suffices ∫ x in A, density κ ν a x s ∂(ν a)
      = limsup (fun i ↦ ∫ x in A, densityProcess κ ν i a x s ∂(ν a)) atTop by
    rw [this, ← limsup_const (α := ℕ) (f := atTop) (∫ x in A, densityProcess κ ν n a x s ∂(ν a)),
      limsup_congr]
    simp only [eventually_atTop]
    refine ⟨n, fun m hnm ↦ ?_⟩
    rw [setIntegral_densityProcess_of_le hκν hnm _ hs hA,
      setIntegral_densityProcess hκν _ _ hs hA]
  -- use L1 convergence
  have h := tendsto_setIntegral_densityProcess hκν a hs A
  rw [h.limsup_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
this : κ = κ'.comapRight h_prod_embed
| κ

Tactic:
rw [this, ← hη']

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
this : κ = κ'.comapRight h_prod_embed
| (κ'.fst ⊗ₖ η).comapRight h_prod_embed
Module: Mathlib.Probability.Kernel.Integral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
a : α
s : Set β
hs : MeasurableSet s
t : Set β
⊢ ∫ (x : β) in t, f x ∂(κ.restrict hs) a = ∫ (x : β) in t ∩ s, f x ∂κ a

Tactic:
rw [restrict_apply, Measure.restrict_restrict' hs]

Goal state after:
Module: Mathlib.Probability.Decision.Risk.Defs

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst✝¹ : Nonempty 𝓧
inst✝ : IsEmpty 𝓨
⊢ minimaxRisk ℓ P = ∞

Tactic:
have : IsEmpty (Subtype (@IsMarkovKernel 𝓧 𝓨 m𝓧 m𝓨)) := by
    simp only [isEmpty_subtype]
    exact fun κ ↦ Subsingleton.elim κ 0 ▸ Kernel.not_isMarkovKernel_zero
  simp [minimaxRisk, iInf_subtype']

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ map (restrict₂ ⋯ ∘ (Iic (I.sup id)).restrict) (infinitePiNat μ) =
    map (restrict₂ ⋯) ((fun I ↦ Measure.pi fun i ↦ μ ↑i) (Iic (I.sup id)))

Tactic:
← map_map,

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ map (restrict₂ ⋯) (map (Iic (I.sup id)).restrict (infinitePiNat μ)) =
    map (restrict₂ ⋯) ((fun I ↦ Measure.pi fun i ↦ μ ↑i) (Iic (I.sup id)))

case hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (restrict₂ ⋯)

case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (Iic (I.sup id)).restrict

X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ MeasurableSpace ((i : ↥(Iic (I.sup id))) → X ↑i)
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)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
⊢ Tendsto (fun n ↦ (piContent μ) (A n)) atTop (𝓝 0)

Tactic:
have : ∀ i, Nonempty (X i) := fun i ↦ nonempty_of_isProbabilityMeasure (μ i)

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
⊢ Tendsto (fun n ↦ (piContent μ) (A n)) atTop (𝓝 0)
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
hm : MeasurableSet (κ.mutuallySingularSetSlice η a)
⊢ ((η.withDensity (κ.rnDeriv η)) a) (s ∩ κ.mutuallySingularSetSlice η a) +
        ((η.withDensity (κ.rnDeriv η)) a) (s \ κ.mutuallySingularSetSlice η a) +
      ((κ a) (s ∩ κ.mutuallySingularSetSlice η a) + ((κ.singularPart η) a) (s \ κ.mutuallySingularSetSlice η a)) =
    (κ a) (s ∩ κ.mutuallySingularSetSlice η a) + (κ a) (s \ κ.mutuallySingularSetSlice η a)

Tactic:
singularPart_of_subset_compl_mutuallySingularSetSlice (sdiff_subset_iff.mpr (by simp)),

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
hm : MeasurableSet (κ.mutuallySingularSetSlice η a)
⊢ ((η.withDensity (κ.rnDeriv η)) a) (s ∩ κ.mutuallySingularSetSlice η a) +
        ((η.withDensity (κ.rnDeriv η)) a) (s \ κ.mutuallySingularSetSlice η a) +
      ((κ a) (s ∩ κ.mutuallySingularSetSlice η a) + 0) =
    (κ a) (s ∩ κ.mutuallySingularSetSlice η a) + (κ a) (s \ κ.mutuallySingularSetSlice η a)
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 b : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
g : ((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n) → ℝ≥0∞ := fun c ↦ f (updateFinset c.2 (Iic b) c.1)
⊢ Measurable fun x₀ ↦
    ∫⁻ (z : (i : ↥(Iic b)) → X ↑i), f (updateFinset x₀ (Iic b) z) ∂(partialTraj κ a b) (frestrictLe a x₀)

Tactic:
let η : Kernel (Π n, X n) (Π i : Iic b, X i) :=
    (partialTraj κ a b).comap (frestrictLe a) (measurable_frestrictLe _)

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
a b : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
g : ((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n) → ℝ≥0∞ := fun c ↦ f (updateFinset c.2 (Iic b) c.1)
η : Kernel ((n : ℕ) → X n) ((i : ↥(Iic b)) → X ↑i) := (partialTraj κ a b).comap (frestrictLe a) ⋯
⊢ Measurable fun x₀ ↦
    ∫⁻ (z : (i : ↥(Iic b)) → X ↑i), f (updateFinset x₀ (Iic b) z) ∂(partialTraj κ a b) (frestrictLe a x₀)
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
| (κ a) univ

Tactic:
rw [← rnDeriv_add_singularPart κ η]

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
| ((η.withDensity (κ.rnDeriv η) + κ.singularPart η) a) univ
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)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ ∏ x ∈ s.attach, (μ ↑x) (if h : ↑x ∈ s then t ⟨↑x, h⟩ else Set.univ) = ∏ i ∈ s.attach, (μ ↑i) (t i)

pp: case a
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ ∀ (i : ι), MeasurableSet (if h : i ∈ s then t ⟨i, h⟩ else Set.univ)

pp: case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ Measurable s.restrict

pp: case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ MeasurableSet (Set.univ.pi t)

Tactic:
· congr with i
    rw [dif_pos i.2]

Goal state after:
case a
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ ∀ (i : ι), MeasurableSet (if h : i ∈ s then t ⟨i, h⟩ else Set.univ)

case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ Measurable s.restrict

case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ MeasurableSet (Set.univ.pi t)