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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : LinearOrder T
R : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid E
inst✝² : Module R E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd E
I : Finset T
x y : Fin #I → E
⊢ (fun i ↦ ∑ j ≤ (I.orderIsoOfFin ⋯).symm i, (x + y) j) =
    (fun i ↦ ∑ j ≤ (I.orderIsoOfFin ⋯).symm i, x j) + fun i ↦ ∑ j ≤ (I.orderIsoOfFin ⋯).symm i, y j

Tactic:
ext; simp [sum_add_distrib]

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

Goal state before:
pp: 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

Tactic:
· exact ⟨h.1.1.1, h.1.1.2, h.1.2, h.2⟩

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

Goal state before:
pp: t : ℚ
⊢ ⨅ r, defaultRatCDF ↑r = defaultRatCDF t

Tactic:
simp only [defaultRatCDF]

Goal state after:
t : ℚ
⊢ (⨅ r, if ↑r < 0 then 0 else 1) = if t < 0 then 0 else 1
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ (hf.stieltjesFunction a).measure univ = 1

Tactic:
← ENNReal.ofReal_one,

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ (hf.stieltjesFunction a).measure univ = ENNReal.ofReal 1
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun X P
⊢ IsGaussian (Measure.map (fun ω x ↦ X x ω) P)

Tactic:
have := hX2.isProbabilityMeasure

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun X P
this : IsProbabilityMeasure P
⊢ IsGaussian (Measure.map (fun ω x ↦ X x ω) P)
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case e_a.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX : HasGaussianLaw (fun ω i ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j → ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)), cov[fun x ↦ L₁ (X i x), fun x ↦ L₂ (X j x); P] = 0
this✝¹ : IsProbabilityMeasure P
this✝ : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this : ∀ (ω : Ω), (L fun x ↦ X x ω) = ∑ i, (L ∘SL single ℝ E i) (X i ω)
⊢ ↑(∫ (ω : Ω), ∑ i, (L ∘SL single ℝ E i) (X i ω) ∂P) = ∑ i, ↑(∫ (ω : Ω), (L ∘SL single ℝ E i) (X i ω) ∂P)

Tactic:
simp_rw [← Complex.ofReal_sum]

Goal state after:
case e_a.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX : HasGaussianLaw (fun ω i ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j → ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)), cov[fun x ↦ L₁ (X i x), fun x ↦ L₂ (X j x); P] = 0
this✝¹ : IsProbabilityMeasure P
this✝ : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this : ∀ (ω : Ω), (L fun x ↦ X x ω) = ∑ i, (L ∘SL single ℝ E i) (X i ω)
⊢ ↑(∫ (ω : Ω), ∑ i, (L ∘SL single ℝ E i) (X i ω) ∂P) = ↑(∑ i, ∫ (ω : Ω), (L ∘SL single ℝ E i) (X i ω) ∂P)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
⊢ ∀ᵐ (a_1 : β) ∂ν a, Antitone fun i ↦ f (a, a_1) (seq i)

Tactic:
filter_upwards [hf.mono a] with t ht using fun n m hnm ↦ ht (hseq hnm)

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
⊢ ∀ᵐ (a_1 : β) ∂ν a, Monotone fun i ↦ f (a, a_1) (seq i)

Tactic:
filter_upwards [hf.mono a] with t ht using fun n m hnm ↦ ht (hseq hnm)

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
⊢ (condCDF ρ a).measure univ = 1

Tactic:
← ENNReal.ofReal_one,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
⊢ (condCDF ρ a).measure univ = ENNReal.ofReal 1
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 t : ℝ≥0
ht : t ≤ t₀
this : IsProbabilityMeasure P
⊢ ↑⟨t, ht⟩ ≤ t₀ + s

pp: case h.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
s t : ℝ≥0
ht : t ≤ t₀
this : IsProbabilityMeasure P
⊢ MemLp (B (t₀ + s)) 2 P

pp: case h.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
s t : ℝ≥0
ht : t ≤ t₀
this : IsProbabilityMeasure P
⊢ MemLp (B t₀) 2 P

pp: case h.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
s t : ℝ≥0
ht : t ≤ t₀
this : IsProbabilityMeasure P
⊢ MemLp (B ↑⟨t, ht⟩) 2 P

Tactic:
· simp [ht, le_add_right]

Goal state after:
case h.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
s t : ℝ≥0
ht : t ≤ t₀
this : IsProbabilityMeasure P
⊢ MemLp (B (t₀ + s)) 2 P

case h.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
s t : ℝ≥0
ht : t ≤ t₀
this : IsProbabilityMeasure P
⊢ MemLp (B t₀) 2 P

case h.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
s t : ℝ≥0
ht : t ≤ t₀
this : IsProbabilityMeasure P
⊢ MemLp (B ↑⟨t, ht⟩) 2 P
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
B : ℝ≥0 → Ω → ℝ
hB : IsBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
⊢ ∀ᵐ (ω : Ω) ∂P, Continuous fun x ↦ (√↑c)⁻¹ * B (c * x) ω

Tactic:
filter_upwards [hB.cont] with ω h
    fun_prop

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
B : ℝ≥0 → Ω → ℝ
hB : IsBrownianReal B P
t₀ : ℝ≥0
⊢ ∀ᵐ (ω : Ω) ∂P, Continuous fun x ↦ B (t₀ + x) ω - B t₀ ω

Tactic:
filter_upwards [hB.cont] with ω h
    fun_prop

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

Goal state before:
pp: β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
⊢ ξ ×ₖ prodMkRight β η ∘ₖ (deterministic f hf ×ₖ κ) = ξ ∘ₖ (deterministic f hf ×ₖ κ) ×ₖ (η ∘ₖ deterministic f hf)

Tactic:
by
  ext ω s hs
  rw [prod_apply' _ _ _ hs, comp_apply' _ _ _ hs, lintegral_deterministic_prod,
    lintegral_comp, lintegral_deterministic_prod]
  · congr with b
    rw [prod_apply' _ _ _ hs, prodMkRight_apply, comp_deterministic_eq_comap, comap_apply]
  · exact (measurable_measure_prodMk_left hs).lintegral_kernel
  · exact measurable_measure_prodMk_left hs
  · exact Kernel.measurable_coe _ hs

Goal state after:
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 α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
⊢ μ ⊗ₘ κ.map f = ⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ ⇑(Kernel.id ×ₖ κ) ∘ₘ μ

Tactic:
comp_assoc,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
⊢ μ ⊗ₘ κ.map f = ⇑(Kernel.id ∥ₖ Kernel.deterministic f hf ∘ₖ (Kernel.id ×ₖ κ)) ∘ₘ μ
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
⊢ ρ ≠ 0

Tactic:
rintro rfl

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρCond : Kernel α Ω
inst✝² : MeasurableSingletonClass α
x : α
s : Set Ω
hs : MeasurableSet s
inst✝¹ : IsCondKernel 0 ρCond
inst✝ : IsFiniteMeasure 0
hx : (fst 0) {x} ≠ 0
⊢ False
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : ¬IsSFiniteKernel κCond
⊢ ∀ᵐ (b : β) ∂κ.fst a, IsProbabilityMeasure (κCond (a, b))

Tactic:
rw [Kernel.compProd_of_not_isSFiniteKernel_right _ _ h_sfin] at h

Goal state after:
case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : 0 = κ
h_sfin : ¬IsSFiniteKernel κCond
⊢ ∀ᵐ (b : β) ∂κ.fst a, IsProbabilityMeasure (κCond (a, b))
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b | r ≤ (κCond (a, b)) univ}
hs : MeasurableSet s
b : β
hbs : b ∈ s
⊢ s.indicator (fun x ↦ r) b ≤ s.indicator (fun b ↦ (κCond (a, b)) univ) b

pp: case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b | r ≤ (κCond (a, b)) univ}
hs : MeasurableSet s
b : β
hbs : b ∉ s
⊢ s.indicator (fun x ↦ r) b ≤ s.indicator (fun b ↦ (κCond (a, b)) univ) b

Tactic:
· simpa [hbs]

Goal state after:
case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b | r ≤ (κCond (a, b)) univ}
hs : MeasurableSet s
b : β
hbs : b ∉ s
⊢ s.indicator (fun x ↦ r) b ≤ s.indicator (fun b ↦ (κCond (a, b)) univ) b
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b | (κCond (a, b)) univ ≤ r}
hs : MeasurableSet s
b : β
hbs : b ∈ s
⊢ s.indicator (fun b ↦ (κCond (a, b)) univ) b ≤ s.indicator (fun x ↦ r) b

pp: case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b | (κCond (a, b)) univ ≤ r}
hs : MeasurableSet s
b : β
hbs : b ∉ s
⊢ s.indicator (fun b ↦ (κCond (a, b)) univ) b ≤ s.indicator (fun x ↦ r) b

Tactic:
· simpa [hbs]

Goal state after:
case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b | (κCond (a, b)) univ ≤ r}
hs : MeasurableSet s
b : β
hbs : b ∉ s
⊢ s.indicator (fun b ↦ (κCond (a, b)) univ) b ≤ s.indicator (fun x ↦ r) b
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond✝ : Kernel (α × β) Ω
inst✝ : Countable α
κCond : α → Kernel β Ω
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
⊢ Measurable fun p ↦ (κCond p.1) p.2

Tactic:
by
    refine measurable_from_prod_countable_right' (fun a ↦ (κCond a).measurable) fun x y hx hy ↦ ?_
    simpa using DFunLike.congr (h_atom _ _ hy) rfl

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 κ b k ∘ₖ partialTraj κ a b = partialTraj κ a (k + 1)

Tactic:
comp_assoc,

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 κ k (k + 1) ∘ₖ (partialTraj κ b k ∘ₖ partialTraj κ a b) = partialTraj κ a (k + 1)
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
⊢ (κ + η).withDensity f = κ.withDensity f + η.withDensity f

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
⊢ (κ + η).withDensity f = κ.withDensity f + η.withDensity f

Tactic:
· ext a s
    simp only [Kernel.withDensity_apply _ hf, add_apply, withDensity_add_measure]

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
⊢ (κ + η).withDensity f = κ.withDensity f + η.withDensity f
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝ : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : (∂κ a/∂η a) x ≤ 1 x
hα : Countable α
⊢ ((∂κ a/∂η a) x).toReal ≤ 1 x

pp: case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝ : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : (∂κ a/∂η a) x ≤ 1 x
hα : ¬Countable α
⊢ (κ.map fun a ↦ (a, ())).density η a x univ ≤ 1 x

Tactic:
· refine ENNReal.toReal_le_of_le_ofReal zero_le_one ?_
    simp only [Pi.one_apply, ENNReal.ofReal_one]
    exact hx_le_one

Goal state after:
case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝ : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : (∂κ a/∂η a) x ≤ 1 x
hα : ¬Countable α
⊢ (κ.map fun a ↦ (a, ())).density η a x univ ≤ 1 x
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)
⊢ IsProjectiveLimit (infinitePiNat μ) fun I ↦ Measure.pi fun i ↦ μ ↑i

Tactic:
intro I
  rw [isProjectiveMeasureFamily_pi μ _ _ I.subset_Iic_sup_id,
    ← restrict₂_comp_restrict I.subset_Iic_sup_id, ← map_map, ← frestrictLe, infinitePiNat,
    map_comp, traj_map_frestrictLe, partialTraj_const, ← map_comp, ← compProd_eq_comp_prod,
    compProd_const, pi_prod_map_IicProdIoc]
  all_goals fun_prop

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✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ (((κ + η).withDensity fun a x ↦ ↑(κ.rnDerivAux (κ + η) a x).toNNReal) a) s = (κ a) s

Tactic:
rw [Kernel.withDensity_apply']

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
⊢ ∫⁻ (b : γ) in s, ↑(κ.rnDerivAux (κ + η) a b).toNNReal ∂(κ + η) a = (κ a) s

case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ Measurable (Function.uncurry fun a x ↦ ↑(κ.rnDerivAux (κ + η) a x).toNNReal)
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 : α
⊢ ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a) = 0

Tactic:
rw [Kernel.withDensity_apply']

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ∫⁻ (b : γ) in κ.mutuallySingularSetSlice η a, κ.rnDeriv η a b ∂η a = 0

case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ Measurable (Function.uncurry (κ.rnDeriv η))
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 η
⊢ MeasurableSet {a | (η.withDensity (κ.rnDeriv η)) a = 0}

Tactic:
withDensity_rnDeriv_eq_zero_iff_measure_eq_zero

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ MeasurableSet {a | (κ a) (κ.mutuallySingularSetSlice η a)ᶜ = 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
x✝ : s.Nonempty
⊢ ((η.withDensity (κ.rnDeriv η)) a) s ≤ (κ a) s

Tactic:
rw [Kernel.withDensity_apply']

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
x✝ : s.Nonempty
⊢ ∫⁻ (b : γ) in s, κ.rnDeriv η a b ∂η a ≤ (κ a) s

case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
x✝ : s.Nonempty
⊢ Measurable (Function.uncurry (κ.rnDeriv η))
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
⊢ (if h : ∀ (i : ι), IsProbabilityMeasure (μ i) then (piContent μ).measure ⋯ ⋯ ⋯ else 0) (I.restrict ⁻¹' s) =
    ((fun I ↦ Measure.pi fun i ↦ μ ↑i) I) s

Tactic:
dif_pos hμ,

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
⊢ ((piContent μ).measure ⋯ ⋯ ⋯) (I.restrict ⁻¹' s) = ((fun I ↦ Measure.pi fun i ↦ μ ↑i) I) s