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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
a : α
⊢ IsRatStieltjesPoint f a ↔
    ((Monotone (f a) ∧ Tendsto (f a) atTop (𝓝 1)) ∧ Tendsto (f a) atBot (𝓝 0)) ∧ ∀ (t : ℚ), ⨅ r, f a ↑r = f a t

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
a : α
h : IsRatStieltjesPoint f a
⊢ ((Monotone (f a) ∧ Tendsto (f a) atTop (𝓝 1)) ∧ Tendsto (f a) atBot (𝓝 0)) ∧ ∀ (t : ℚ), ⨅ r, f a ↑r = f a t

case refine_2
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
a : α
h : ((Monotone (f a) ∧ Tendsto (f a) atTop (𝓝 1)) ∧ Tendsto (f a) atBot (𝓝 0)) ∧ ∀ (t : ℚ), ⨅ r, f a ↑r = f a t
⊢ IsRatStieltjesPoint f a
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
⊢ IsPreBrownianReal (fun t ω ↦ B (t₀ + t) ω - B t₀ ω) P

Tactic:
by
  refine (hB.isGaussianProcess.shift t₀).isPreBrownianReal_of_covariance
    (fun t ↦ ?_) (fun s t hst ↦ ?_)
  · rw [integral_sub, hB.integral_eval, hB.integral_eval, sub_zero]
    all_goals exact (hB.isGaussianProcess.hasGaussianLaw_eval _).integrable
  · have := hB.isGaussianProcess.isProbabilityMeasure
    rw [covariance_fun_sub_left, covariance_fun_sub_right, covariance_fun_sub_right,
      hB.covariance_eval, hB.covariance_eval, hB.covariance_eval, hB.covariance_eval, ← add_min,
      min_eq_left hst, min_eq_right, min_eq_left, min_self]
    any_goals simp
    any_goals exact (hB.isGaussianProcess.hasGaussianLaw_eval _).memLp_two
    exact hB.isGaussianProcess.hasGaussianLaw_sub.memLp_two

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: case convert_7
Ω : 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 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
mX0 : AEMeasurable (X 0) P
intX0 : Integrable (X 0) P
this :
  ∀ (n : ℕ) (ω : Ω),
    (√(↑n * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P) =
      (√↑n)⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]
⊢ Var[X 0; P] / √Var[X 0; P] ^ 2 = 1

Tactic:
Real.sq_sqrt (variance_nonneg _ _),

Goal state after:
case convert_7
Ω : 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 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
mX0 : AEMeasurable (X 0) P
intX0 : Integrable (X 0) P
this :
  ∀ (n : ℕ) (ω : Ω),
    (√(↑n * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P) =
      (√↑n)⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]
⊢ Var[X 0; P] / Var[X 0; P] = 1
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : CompleteSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : CompleteSpace F
inst✝³ : BorelSpace F
inst✝² : SecondCountableTopology F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (fun ω ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[⇑L₁ ∘ X, ⇑L₂ ∘ Y; P] = 0
⊢ X ⟂ᵢ[P] Y

Tactic:
have := hXY.isProbabilityMeasure

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : CompleteSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : CompleteSpace F
inst✝³ : BorelSpace F
inst✝² : SecondCountableTopology F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (fun ω ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[⇑L₁ ∘ X, ⇑L₂ ∘ Y; P] = 0
this : IsProbabilityMeasure P
⊢ X ⟂ᵢ[P] Y
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:

Tactic:
μ ⊗ₘ (κ.map f)
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.id ×ₖ κ) ∘ₘ μ := by
    rw [comp_assoc, Kernel.parallelComp_comp_prod, compProd_eq_comp_prod,
      Kernel.id_comp, Kernel.deterministic_comp_eq_map]
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (μ ⊗ₘ κ) := by rw [compProd_eq_comp_prod]
  _ = (μ ⊗ₘ κ).map (Prod.map id f) := by
    rw [Kernel.id, Kernel.deterministic_parallelComp_deterministic, deterministic_comp_eq_map]

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

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
hs : MeasurableSet s
this✝ : IsSFiniteKernel ρCond
this : ∀ (a : α), (ρCond a) (Prod.mk a ⁻¹' {x} ×ˢ s) = {x}.indicator (fun x ↦ (ρCond x) s) a
⊢ (ρCond x) s = (ρ.fst {x})⁻¹ * (ρ.fst {x} * (ρCond x) s)

Tactic:
rw [← mul_assoc, ENNReal.inv_mul_cancel hx (measure_ne_top _ _), one_mul]

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 ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq : ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' t) ∂ν a = (κ a) t
⊢ ∫⁻ (b : β),
      ((IsCondKernelCDF.toKernel f hf) (a, b)) univ - ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' t) ∂ν a =
    ∫⁻ (x : β), ((IsCondKernelCDF.toKernel f hf) (a, x)) univ ∂ν a -
      ∫⁻ (x : β), ((IsCondKernelCDF.toKernel f hf) (a, x)) (Prod.mk x ⁻¹' t) ∂ν a

Tactic:
by
        have h_le : (fun x ↦ hf.toKernel f (a, x) (Prod.mk x ⁻¹' t))
              ≤ᵐ[ν a] fun x ↦ hf.toKernel f (a, x) univ :=
          Eventually.of_forall fun _ ↦ measure_mono (subset_univ _)
        rw [lintegral_sub _ _ h_le]
        · exact Kernel.measurable_kernel_prodMk_left' ht a
        refine ((lintegral_mono_ae h_le).trans_lt ?_).ne
        rw [lintegral_toKernel_univ hf]
        exact measure_lt_top _ univ

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (fun i ↦ X i ω, fun j ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
⊢ (fun ω i ↦ X i ω) ⟂ᵢ[P] fun ω j ↦ Y j ω

Tactic:
have := hXY.isProbabilityMeasure

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (fun i ↦ X i ω, fun j ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this : IsProbabilityMeasure P
⊢ (fun ω i ↦ X i ω) ⟂ᵢ[P] fun ω j ↦ Y j ω
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this✝ : IsFiniteKernel κ
hu_meas : MeasurableSet u
this :
  ∫⁻ (x : γ) in u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ∂ν a =
    ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a
h0 : (ν a) u = 0
h0' : (κ a) {p | p.1 ∈ u} = 0
⊢ u ×ˢ s ⊆ {p | p.1 ∈ u}

Tactic:
intro p

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this✝ : IsFiniteKernel κ
hu_meas : MeasurableSet u
this :
  ∫⁻ (x : γ) in u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ∂ν a =
    ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a
h0 : (ν a) u = 0
h0' : (κ a) {p | p.1 ∈ u} = 0
p : γ × β
⊢ p ∈ u ×ˢ s → p ∈ {p | p.1 ∈ u}
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this✝ : IsFiniteKernel κ
hu_meas : MeasurableSet u
this :
  ∫⁻ (x : γ) in u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ∂ν a =
    ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a
h0 : (ν a) u = 0
⊢ (κ a) (u ×ˢ s) / (ν a) u * (ν a) u = (κ a) (u ×ˢ s)

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this✝ : IsFiniteKernel κ
hu_meas : MeasurableSet u
this :
  ∫⁻ (x : γ) in u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ∂ν a =
    ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a
h0 : ¬(ν a) u = 0
⊢ (κ a) (u ×ˢ s) / (ν a) u * (ν a) u = (κ a) (u ×ˢ s)

Tactic:
· simp only [h0, mul_zero]
    have h0' : fst κ a u = 0 := by simpa using (hκν a _).trans h0.le
    rw [fst_apply' _ _ hu_meas] at h0'
    refine (measure_mono_null ?_ h0').symm
    intro p
    simp only [mem_prod, mem_ofPred_eq, and_imp]
    exact fun h _ ↦ h

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this✝ : IsFiniteKernel κ
hu_meas : MeasurableSet u
this :
  ∫⁻ (x : γ) in u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ∂ν a =
    ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a
h0 : ¬(ν a) u = 0
⊢ (κ a) (u ×ˢ s) / (ν a) u * (ν a) u = (κ a) (u ×ˢ s)
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel

Tactic:
rw [setLIntegral_compProd hf hs ht]

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

Goal state before:
pp: β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (Set.univ ×ˢ t) ρ
⊢ ∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in Set.univ ×ˢ t, f x ∂ρ

Tactic:
← setIntegral_condKernel MeasurableSet.univ ht hf

Goal state after:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (Set.univ ×ˢ t) ρ
⊢ ∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫ (b : β) in Set.univ, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
s : Set (α × ℝ)
hs : MeasurableSet s
⊢ (ρ.fst ⊗ₘ κ) (Prod.map id (embeddingReal Ω) ⁻¹' s) = ∫⁻ (a : α), ((κ.map f) a) (Prod.mk a ⁻¹' s) ∂ρ.fst

Tactic:
Measure.compProd_apply (measurable_id.prodMap hf.measurable hs)

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
s : Set (α × ℝ)
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' Prod.map id (embeddingReal Ω) ⁻¹' s) ∂ρ.fst =
    ∫⁻ (a : α), ((κ.map f) a) (Prod.mk a ⁻¹' s) ∂ρ.fst
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : DecidableLE ι
X : ι → Type u_2
a b c : ι
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
x : ((i : ↥(Ioc a b)) → X ↑i) × ((i : ↥(Ioc b c)) → X ↑i)
⊢ (∀ (a_1 : ι) (hp : a < a_1) (hq : a_1 ≤ c), IocProdIoc a b c x ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩) ↔
    (∀ (a_1 : ι) (hp : a < a_1) (hq : a_1 ≤ b), x.1 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩) ∧
      ∀ (a_1 : ι) (hp : b < a_1) (hq : a_1 ≤ c), x.2 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩

Tactic:
grind [IocProdIoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
⊢ ∀ᵐ (b : β) ∂Measure.map X μ, Integrable (fun ω ↦ f (b, ω)) ((Measure.map (fun a ↦ (X a, Y a)) μ).condKernel b)

Tactic:
← Measure.fst_map_prodMk₀ (X := X) hY

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
⊢ ∀ᵐ (b : β) ∂(Measure.map (fun a ↦ (X a, Y a)) μ).fst,
    Integrable (fun ω ↦ f (b, ω)) ((Measure.map (fun a ↦ (X a, Y a)) μ).condKernel b)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
⊢ Integrable (fun x ↦ ∫ (y : Ω), ‖f (x, y)‖ ∂(Measure.map (fun a ↦ (X a, Y a)) μ).condKernel x) (Measure.map X μ)

Tactic:
← Measure.fst_map_prodMk₀ (X := X) hY

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
⊢ Integrable (fun x ↦ ∫ (y : Ω), ‖f (x, y)‖ ∂(Measure.map (fun a ↦ (X a, Y a)) μ).condKernel x)
    (Measure.map (fun a ↦ (X a, Y a)) μ).fst
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝ : NormedSpace ℝ F
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
⊢ Integrable (fun x ↦ ‖∫ (y : Ω), f (x, y) ∂(Measure.map (fun a ↦ (X a, Y a)) μ).condKernel x‖) (Measure.map X μ)

Tactic:
← Measure.fst_map_prodMk₀ (X := X) hY

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝ : NormedSpace ℝ F
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
⊢ Integrable (fun x ↦ ‖∫ (y : Ω), f (x, y) ∂(Measure.map (fun a ↦ (X a, Y a)) μ).condKernel x‖)
    (Measure.map (fun a ↦ (X a, Y a)) μ).fst
Module: Mathlib.Probability.Kernel.Integral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : β → E
a : α
inst✝¹ : CompleteSpace E
g : α → β
inst✝ : MeasurableSingletonClass β
hg : Measurable g
⊢ ∫ (x : β), f x ∂(deterministic g hg) a = f (g a)

Tactic:
rw [deterministic_apply, integral_dirac _ (g a)]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
E : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
κ : Kernel X Y
μ : Measure X
f : X → Y → E
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X), ∫ (y : Y), s.indicator (fun x ↦ f x y) x ∂κ x ∂μ = ∫ (x : X) in s, ∫ (y : Y), f x y ∂κ x ∂μ

Tactic:
by
  simp_rw [← integral_indicator hs, Kernel.integral_indicator₂]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case refine_1
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X ↑i)
ms : ∀ (i : ↥J), MeasurableSet (s i)
x : ι
hx : x ∈ I \ J
⊢ Function.extend Subtype.val (fun i ↦ (μ ↑i) (if h : ↑i ∈ J then s ⟨↑i, h⟩ else Set.univ)) 1 x = 1

Tactic:
Function.extend_val_apply (mem_sdiff.1 hx).1,

Goal state after:
case refine_1
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X ↑i)
ms : ∀ (i : ↥J), MeasurableSet (s i)
x : ι
hx : x ∈ I \ J
⊢ (μ ↑⟨x, ⋯⟩) (if h : ↑⟨x, ⋯⟩ ∈ J then s ⟨↑⟨x, ⋯⟩, h⟩ else Set.univ) = 1
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
aux₁ : Integrable (2 * X * μ[X | m]) μ
aux₂ : Integrable (μ[X | m] ^ 2) μ
ω : Ω
hω₀ : μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] ω = (μ[X ^ 2 - 2 * X * μ[X | m] | m] + μ[μ[X | m] ^ 2 | m]) ω
⊢ μ[X ^ 2 - 2 * X * μ[X | m] | m] ω = (μ[X ^ 2 | m] - μ[2 * X * μ[X | m] | m]) ω →
    μ[2 * X * μ[X | m] | m] ω = (μ[2 * X | m] * μ[X | m]) ω →
      μ[OfNat.ofNat 2 * X | m] ω = (OfNat.ofNat 2 * μ[X | m]) ω →
        μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] ω = (μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2) ω

Tactic:
hω₁

Goal state after:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
aux₁ : Integrable (2 * X * μ[X | m]) μ
aux₂ : Integrable (μ[X | m] ^ 2) μ
ω : Ω
hω₀ : μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] ω = (μ[X ^ 2 - 2 * X * μ[X | m] | m] + μ[μ[X | m] ^ 2 | m]) ω
hω₁ : μ[X ^ 2 - 2 * X * μ[X | m] | m] ω = (μ[X ^ 2 | m] - μ[2 * X * μ[X | m] | m]) ω
⊢ μ[2 * X * μ[X | m] | m] ω = (μ[2 * X | m] * μ[X | m]) ω →
    μ[OfNat.ofNat 2 * X | m] ω = (OfNat.ofNat 2 * μ[X | m]) ω →
      μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] ω = (μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2) ω
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 : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
n : ℕ
⊢ Measurable (χ n)

Tactic:
simp_rw [χ, A_eq]

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 : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
n : ℕ
⊢ Measurable ((cylinder (Iic (a n)) (S n)).indicator 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 : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
n : ℕ
⊢ DependsOn (χ n) ↑(Iic (a n))

Tactic:
simp_rw [χ, A_eq]

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 : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
n : ℕ
⊢ DependsOn ((cylinder (Iic (a n)) (S n)).indicator 1) ↑(Iic (a n))