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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
μ : Measure E
inst✝ : IsGaussian μ
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
⊢ Integrable (fun x ↦ rexp (C / 2 * ‖x‖ ^ 2)) μ

Tactic:
exact integrable_exp_sq_of_conv_neg μ hC (by positivity) (by simp [hC_pos])

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ multivariateGaussian 0 1 = stdGaussian (EuclideanSpace ℝ ι)

Tactic:
by
  simp [multivariateGaussian]

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
p : ℝ≥0∞
inst✝⁸ : Fact (1 ≤ p)
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), BorelSpace (E i)
inst✝² : ∀ (i : ι), SecondCountableTopology (E i)
X : (i : ι) → Ω → E i
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
inst✝ : DecidableEq ι
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ iIndepFun X P ↔
    ∀ (L : StrongDual ℝ (WithLp p ((x : ι) → E x))),
      charFunDual (Measure.map (fun ω ↦ toLp p fun x ↦ X x ω) P) L =
        ∏ i,
          charFunDual (Measure.map (X i) P)
            (L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E i)

Tactic:
by
  rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFunDual_eq_pi_iff' p,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]

Goal state after:
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 α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (fun i ω j ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᵐ[κ a] X' i j
s : Finset S
f : S → Set Ω
g : (i : S) → Set ((fun i ↦ (j : T i) → 𝓧 i j) i)
mg : ∀ i ∈ s, MeasurableSet (g i)
hg : ∀ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i = f i
h3 : ⋂ i ∈ s, f i = ⋂ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i
h3' : ∀ (a : α), ∏ i ∈ s, (κ a) (f i) = ∏ i ∈ s, (κ a) ((fun i ω j ↦ X' i j ω) i ⁻¹' g i)
I : (i : S) → Set (T i)
u : (i : S) → Set ((a : ↑(I i)) → 𝓧 i ↑a)
hI : ∀ i ∈ s, (I i).Countable
hu : ∀ i ∈ s, g i = (I i).domRestrict ⁻¹' u i
h4 :
  ∀ (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
    ⋂ i ∈ s, (fun i ω j ↦ f i j ω) i ⁻¹' g i = ⋂ i ∈ s, (fun i ω j ↦ f i j ω) i ⁻¹' (I i).domRestrict ⁻¹' u i
h4' :
  ∀ (a : α) (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
    ∏ i ∈ s, (κ a) ((fun i ω j ↦ f i j ω) i ⁻¹' g i) =
      ∏ i ∈ s, (κ a) ((fun i ω j ↦ f i j ω) i ⁻¹' (I i).domRestrict ⁻¹' u i)
⊢ ∀ᵐ (a : α) ∂P, (κ a) (⋂ i ∈ s, (fun ω j ↦ X' i j ω) ⁻¹' g i) = ∏ x ∈ s, (κ a) ((fun ω j ↦ X' x j ω) ⁻¹' g x)

Tactic:
have h5 := h1 s (fun i hi ↦ ⟨g i, mg i hi, rfl⟩)

Goal state after:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (fun i ω j ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᵐ[κ a] X' i j
s : Finset S
f : S → Set Ω
g : (i : S) → Set ((fun i ↦ (j : T i) → 𝓧 i j) i)
mg : ∀ i ∈ s, MeasurableSet (g i)
hg : ∀ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i = f i
h3 : ⋂ i ∈ s, f i = ⋂ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i
h3' : ∀ (a : α), ∏ i ∈ s, (κ a) (f i) = ∏ i ∈ s, (κ a) ((fun i ω j ↦ X' i j ω) i ⁻¹' g i)
I : (i : S) → Set (T i)
u : (i : S) → Set ((a : ↑(I i)) → 𝓧 i ↑a)
hI : ∀ i ∈ s, (I i).Countable
hu : ∀ i ∈ s, g i = (I i).domRestrict ⁻¹' u i
h4 :
  ∀ (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
    ⋂ i ∈ s, (fun i ω j ↦ f i j ω) i ⁻¹' g i = ⋂ i ∈ s, (fun i ω j ↦ f i j ω) i ⁻¹' (I i).domRestrict ⁻¹' u i
h4' :
  ∀ (a : α) (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
    ∏ i ∈ s, (κ a) ((fun i ω j ↦ f i j ω) i ⁻¹' g i) =
      ∏ i ∈ s, (κ a) ((fun i ω j ↦ f i j ω) i ⁻¹' (I i).domRestrict ⁻¹' u i)
h5 : ∀ᵐ (a : α) ∂P, (κ a) (⋂ i ∈ s, (fun i ω j ↦ X i j ω) i ⁻¹' g i) = ∏ i ∈ s, (κ a) ((fun i ω j ↦ X i j ω) i ⁻¹' g i)
⊢ ∀ᵐ (a : α) ∂P, (κ a) (⋂ i ∈ s, (fun ω j ↦ X' i j ω) ⁻¹' g i) = ∏ x ∈ s, (κ a) ((fun ω j ↦ X' x j ω) ⁻¹' g x)
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
f : α → StieltjesFunction ℝ
hf : ∀ (q : ℝ), Measurable fun a ↦ ↑(f a) q
hf_bot : ∀ (a : α), Tendsto (↑(f a)) atBot (𝓝 0)
hf_top : ∀ (a : α), Tendsto (↑(f a)) atTop (𝓝 1)
this : ∀ (a : α), IsProbabilityMeasure (f a).measure
⊢ ∀ s ∈ range Iic, Measurable fun a ↦ (f a).measure s

Tactic:
simp_rw [forall_mem_range, StieltjesFunction.measure_Iic (f _) (hf_bot _), sub_zero]

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
f : α → StieltjesFunction ℝ
hf : ∀ (q : ℝ), Measurable fun a ↦ ↑(f a) q
hf_bot : ∀ (a : α), Tendsto (↑(f a)) atBot (𝓝 0)
hf_top : ∀ (a : α), Tendsto (↑(f a)) atTop (𝓝 1)
this : ∀ (a : α), IsProbabilityMeasure (f a).measure
⊢ ∀ (i : ℝ), Measurable fun a ↦ ENNReal.ofReal (↑(f a) i)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case hfi
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q) ((ν a).restrict s)

Tactic:
refine Integrable.restrict ?_

Goal state after:
case hfi
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q) (ν a)
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x ↦ ⋯.choose
q : ℚ
y : ℝ
hy : ↑q + 1 ≤ y
h_le : y - 1 ≤ ↑(qs y)
⊢ q ≤ qs y

Tactic:
sub_le_iff_le_add

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x ↦ ⋯.choose
q : ℚ
y : ℝ
hy : ↑q + 1 ≤ y
h_le : y ≤ ↑(qs y) + 1
⊢ q ≤ qs y
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
⊢ IsPreBrownianReal (-B) P

Tactic:
refine HasIndepIncrements.isPreBrownianReal_of_hasLaw (fun t ↦ ?_) (fun n t ht ↦ ?_)
  · simpa using gaussianReal_neg (hB.hasLaw_eval t)
  convert (hB.hasIndepIncrements n t ht).comp (fun _ x ↦ -x) (by fun_prop)
  simp
  grind

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: case e_f.e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
a : α
b : β
⊢ (κ b) (Prod.mk a ⁻¹' s) = ((Kernel.id ∥ₖ κ) (a, b)) s

Tactic:
rw [Kernel.parallelComp_apply, Kernel.id_apply, Measure.prod_apply hs, lintegral_dirac']

Goal state after:
case e_f.e_f.hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
a : α
b : β
⊢ Measurable fun x ↦ (κ (a, b).2) (Prod.mk x ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝² : SFinite μ
inst✝¹ : SFinite ν
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
h1 : (⇑κ ∘ₘ μ).prod ν = map Prod.swap (ν.prod (⇑κ ∘ₘ μ))
h2 : ⇑(κ ∥ₖ Kernel.id) ∘ₘ μ.prod ν = map Prod.swap (⇑(Kernel.id ∥ₖ κ) ∘ₘ ν.prod μ)
⊢ (⇑κ ∘ₘ μ).prod ν = ⇑(κ ∥ₖ Kernel.id) ∘ₘ μ.prod ν

Tactic:
← Measure.prod_comp_right,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝² : SFinite μ
inst✝¹ : SFinite ν
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
h1 : (⇑κ ∘ₘ μ).prod ν = map Prod.swap (ν.prod (⇑κ ∘ₘ μ))
h2 : ⇑(κ ∥ₖ Kernel.id) ∘ₘ μ.prod ν = map Prod.swap (ν.prod (⇑κ ∘ₘ μ))
⊢ (⇑κ ∘ₘ μ).prod ν = ⇑(κ ∥ₖ Kernel.id) ∘ₘ μ.prod ν
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 κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
hf : AEStronglyMeasurable f (κ a)
⊢ AEStronglyMeasurable (fun x ↦ ∫ (y : Ω), f (x, y) ∂κ.condKernel (a, x)) (κ.fst a)

Tactic:
rw [← κ.disintegrate κ.condKernel] at hf

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
hf : AEStronglyMeasurable f ((κ.fst ⊗ₖ κ.condKernel) a)
⊢ AEStronglyMeasurable (fun x ↦ ∫ (y : Ω), f (x, y) ∂κ.condKernel (a, x)) (κ.fst a)
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 κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
hf : Integrable f (κ a)
⊢ ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω), f x ∂(κ.fst ⊗ₖ κ.condKernel) a

Tactic:
rw [← κ.disintegrate κ.condKernel] at hf

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
hf : Integrable f ((κ.fst ⊗ₖ κ.condKernel) a)
⊢ ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω), f x ∂(κ.fst ⊗ₖ κ.condKernel) a
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 κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) (κ a)
⊢ ∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫ (x : β × Ω) in s ×ˢ t, f x ∂(κ.fst ⊗ₖ κ.condKernel) a

Tactic:
rw [← κ.disintegrate κ.condKernel] at hf

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝² : IsFiniteKernel κ
E : Type u_4
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ((κ.fst ⊗ₖ κ.condKernel) a)
⊢ ∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫ (x : β × Ω) in s ×ˢ t, f x ∂(κ.fst ⊗ₖ κ.condKernel) a
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ κ.densityProcess ν n a x s

pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ κ.densityProcess ν n a x s'

Tactic:
· exact isCoboundedUnder_le_of_le atTop (fun i ↦ densityProcess_nonneg _ _ _ _ _ _)

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ κ.densityProcess ν n a x s'
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s : Set β
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ κ.densityProcess ν n a x s

pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s : Set β
⊢ ∀ᶠ (n : ℕ) in atTop, κ.densityProcess ν n a x s ≤ 1

Tactic:
· exact isCoboundedUnder_le_of_le atTop (fun i ↦ densityProcess_nonneg _ _ _ _ _ _)

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s : Set β
⊢ ∀ᶠ (n : ℕ) in atTop, κ.densityProcess ν n a x s ≤ 1
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
s : Set β
hs : MeasurableSet s
⊢ (Measure.map X μ) s = (Measure.map (fun x ↦ (X x, Y x)) μ).fst s

Tactic:
rw [Measure.map_apply hX hs, Measure.fst_apply hs, Measure.map_apply]

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
s : Set β
hs : MeasurableSet s
⊢ μ (X ⁻¹' s) = μ ((fun x ↦ (X x, Y x)) ⁻¹' Prod.fst ⁻¹' s)

case hf
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
s : Set β
hs : MeasurableSet s
⊢ Measurable fun x ↦ (X x, Y x)

case hs
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (Prod.fst ⁻¹' s)
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hba : b ≤ a
⊢ partialTraj κ a b = deterministic (frestrictLe₂ hba) ⋯

Tactic:
rw [partialTraj, dif_pos hba]

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

Goal state before:
pp: case succ
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab : a ≤ b
k : ℕ
h : b ≤ k
hk : partialTraj κ b k ∘ₖ partialTraj κ a b = partialTraj κ a k
⊢ partialTraj κ k (k + 1) ∘ₖ partialTraj κ a k = partialTraj κ a (k + 1)

Tactic:
← partialTraj_succ_eq_comp (hab.trans h)

Goal state after:
case succ
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab : a ≤ b
k : ℕ
h : b ≤ k
hk : partialTraj κ b k ∘ₖ partialTraj κ a b = partialTraj κ a k
⊢ partialTraj κ a (k + 1) = partialTraj κ a (k + 1)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measure.map (restrict₂ this) (Measure.map (Iic (max (I.sup id) a)).restrict ν) = μ I

pp: case hg
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measurable (restrict₂ this)

pp: case hf
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measurable (Iic (max (I.sup id) a)).restrict

pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ MeasurableSpace ((i : ↥(Iic (max (I.sup id) a))) → X ↑i)

Tactic:
← frestrictLe,

Goal state after:
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measure.map (restrict₂ this) (Measure.map (frestrictLe (max (I.sup id) a)) ν) = μ I

case hg
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measurable (restrict₂ this)

case hf
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measurable (Iic (max (I.sup id) a)).restrict

X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ MeasurableSpace ((i : ↥(Iic (max (I.sup id) a))) → X ↑i)
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)
⊢ IsProbabilityMeasure (infinitePiNat μ)

Tactic:
Measure.infinitePiNat

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
⊢ IsProbabilityMeasure (⇑(traj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) 0) ∘ₘ Measure.pi fun i ↦ μ ↑i)
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₂ ⋯) (map (Iic (I.sup id)).restrict (infinitePiNat μ)) =
    map (restrict₂ ⋯) ((fun I ↦ Measure.pi fun i ↦ μ ↑i) (Iic (I.sup id)))

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

pp: 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

pp: 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)

Tactic:
← frestrictLe,

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 (frestrictLe (I.sup id)) (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)
I : Finset ι
s : Set ((i : ↥I) → X ↑i)
hs : MeasurableSet s
⊢ (infinitePi μ) (I.restrict ⁻¹' s) = ((fun I ↦ Measure.pi fun i ↦ μ ↑i) I) s

Tactic:
infinitePi,

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I : Finset ι
s : Set ((i : ↥I) → X ↑i)
hs : MeasurableSet s
⊢ (if h : ∀ (i : ι), IsProbabilityMeasure (μ i) then (piContent μ).measure ⋯ ⋯ ⋯ else 0) (I.restrict ⁻¹' s) =
    ((fun I ↦ Measure.pi fun i ↦ μ ↑i) I) s
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
a✝¹ : ∀ (a : α), IsZeroOneMeasure (κ a)
a✝ : α
⊢ (κ a✝).prod (κ a✝) = (copy β ∘ₖ κ) a✝

Tactic:
refine Measure.prod_eq fun s t hs ht ↦ ?_

Goal state after:
case mpr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
a✝¹ : ∀ (a : α), IsZeroOneMeasure (κ a)
a✝ : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((copy β ∘ₖ κ) a✝) (s ×ˢ t) = (κ a✝) s * (κ a✝) t