mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
⊢ covarianceBilinDual 0 = 0

Tactic:
covarianceBilinDual,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
⊢ uncenteredCovarianceBilinDual (Measure.map (fun x ↦ x - ∫ (x : E), x ∂0) 0) = 0
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp (fun x ↦ x - ∫ (y : E), y ∂μ) 2 μ
h' : MemLp id 2 (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ)
⊢ ((covarianceBilinDual μ) L₁) L₂ = ((covarianceBilinDual μ) L₂) L₁

Tactic:
covarianceBilinDual,

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp (fun x ↦ x - ∫ (y : E), y ∂μ) 2 μ
h' : MemLp id 2 (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ)
⊢ ((uncenteredCovarianceBilinDual (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ)) L₁) L₂ =
    ((uncenteredCovarianceBilinDual (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ)) L₂) L₁
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), L₁ x ∂μ) * (L₂ x - ∫ (x : E), L₂ x ∂μ) ∂μ

Tactic:
covarianceBilinDual,

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
⊢ ((uncenteredCovarianceBilinDual (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ)) L₁) L₂ =
    ∫ (x : E), (L₁ x - ∫ (x : E), L₁ x ∂μ) * (L₂ x - ∫ (x : E), L₂ x ∂μ) ∂μ
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ ∫ (x : EuclideanSpace ℝ ι),
      x ∂Measure.map (fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x) (stdGaussian (EuclideanSpace ℝ ι)) =
    μ

Tactic:
integral_map (by fun_prop) (by fun_prop),

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ ∫ (x : EuclideanSpace ℝ ι), μ + (toEuclideanCLM (CFC.sqrt S)) x ∂stdGaussian (EuclideanSpace ℝ ι) = μ
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✝² : CompleteSpace E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (t : E),
    charFun (Measure.map X P) t = cexp (↑(∫ (x : Ω), (fun ω ↦ ⟪t, X ω⟫) x ∂P) * I - ↑Var[fun ω ↦ ⟪t, X ω⟫; P] / 2)
⊢ HasGaussianLaw X P

Tactic:
refine ⟨isGaussian_iff_charFun_eq.2 fun t ↦ ?_⟩
    rw [h, integral_map, variance_map, integral_complex_ofReal, Function.comp_def]
    all_goals fun_prop

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

Goal state before:
pp: I : Finset ℝ≥0
s t : ↥I
hst : ↑s ≤ ↑t
⊢ ↑s - ↑t ≤ ↑t - ↑s

Tactic:
by grw [hst]

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h : ∀ (t : T), X t =ᵐ[P] Y t
⊢ Measure.map (fun ω x ↦ X x ω) P = Measure.map (fun ω x ↦ Y x ω) P

Tactic:
by
  rw [map_eq_iff_forall_finset_map_restrict_eq hX hY]
  exact fun I ↦ map_restrict_eq_of_forall_ae_eq h I

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : T → Type u_4
X : (t : T) → S t → Ω → E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess (fun p ω ↦ X p.fst p.snd ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X t₁ s₁, ⇑L₂ ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
⊢ iIndepFun (fun t ω s ↦ X t s ω) P

Tactic:
refine iIndepFun.iIndepFun_process₀ mX fun I J ↦
    HasGaussianLaw.iIndepFun_of_covariance_strongDual ?_ fun i j hij L₁ L₂ ↦ ?_
  · let L : (I.sigma (fun i ↦ if hi : i ∈ I then J ⟨i, hi⟩ else ∅) → E) →L[ℝ] (i : I) → J i → E :=
      { toFun x i j := x ⟨⟨i, j⟩, by simp⟩
        map_add' x y := by ext; simp
        map_smul' c x := by ext; simp }
    exact (hX.hasGaussianLaw _).map L
  have h1 : L₁ ∘ (fun ω k ↦ X i k ω) = ∑ k : J i, (L₁ ∘L .single ℝ _ k) ∘ X i k := by
    ext; simp [-ContinuousLinearMap.comp_apply, ← L₁.sum_comp_single]
  have h2 : L₂ ∘ (fun ω k ↦ X j k ω) = ∑ k : J j, (L₂ ∘L .single ℝ _ k) ∘ X j k := by
    ext; simp [-ContinuousLinearMap.comp_apply, ← L₂.sum_comp_single]
  rw [h1, h2, covariance_sum_sum]
  · exact sum_eq_zero fun _ _ ↦ sum_eq_zero fun _ _ ↦ h i j (by simpa) ..
  · exact fun k ↦ ((hX.hasGaussianLaw_eval ⟨i, k⟩).map _).memLp_two
  · exact fun k ↦ ((hX.hasGaussianLaw_eval ⟨j, k⟩).map _).memLp_two

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

Goal state before:
pp: case hbc
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
L✝ L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ ((i : ι) → E i)) :=
  LinearMap.mk₂ ℝ (fun x y ↦ ∑ i, ((L i) (x ∘SL single ℝ E i)) (y ∘SL single ℝ E i)) ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ ((i : ι) → E i)
i : ι
a✝ : i ∈ univ
⊢ ‖x‖ * 1 ≤ ‖x‖

Tactic:
mul_one

Goal state after:
case hbc
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
L✝ L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ ((i : ι) → E i)) :=
  LinearMap.mk₂ ℝ (fun x y ↦ ∑ i, ((L i) (x ∘SL single ℝ E i)) (y ∘SL single ℝ E i)) ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ ((i : ι) → E i)
i : ι
a✝ : i ∈ univ
⊢ ‖x‖ ≤ ‖x‖
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case h₂
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
L✝ L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ ((i : ι) → E i)) :=
  LinearMap.mk₂ ℝ (fun x y ↦ ∑ i, ((L i) (x ∘SL single ℝ E i)) (y ∘SL single ℝ E i)) ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ ((i : ι) → E i)
i : ι
a✝ : i ∈ univ
⊢ ‖y‖ * 1 ≤ ‖y‖

Tactic:
mul_one

Goal state after:
case h₂
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
L✝ L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ ((i : ι) → E i)) :=
  LinearMap.mk₂ ℝ (fun x y ↦ ∑ i, ((L i) (x ∘SL single ℝ E i)) (y ∘SL single ℝ E i)) ⋯ ⋯ ⋯ ⋯
x y : StrongDual ℝ ((i : ι) → E i)
i : ι
a✝ : i ∈ univ
⊢ ‖y‖ ≤ ‖y‖
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case hbc
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
L₁✝ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂✝ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ (fun x y ↦ (L₁ (x ∘SL inl ℝ E F)) (y ∘SL inl ℝ E F) + (L₂ (x ∘SL inr ℝ E F)) (y ∘SL inr ℝ E F)) ⋯ ⋯ ⋯
    ⋯
x y : StrongDual ℝ (E × F)
⊢ ‖x‖ * 1 ≤ ‖x‖

Tactic:
mul_one

Goal state after:
case hbc
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
L₁✝ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂✝ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ (fun x y ↦ (L₁ (x ∘SL inl ℝ E F)) (y ∘SL inl ℝ E F) + (L₂ (x ∘SL inr ℝ E F)) (y ∘SL inr ℝ E F)) ⋯ ⋯ ⋯
    ⋯
x y : StrongDual ℝ (E × F)
⊢ ‖x‖ ≤ ‖x‖
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case h₂
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
L₁✝ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂✝ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ (fun x y ↦ (L₁ (x ∘SL inl ℝ E F)) (y ∘SL inl ℝ E F) + (L₂ (x ∘SL inr ℝ E F)) (y ∘SL inr ℝ E F)) ⋯ ⋯ ⋯
    ⋯
x y : StrongDual ℝ (E × F)
⊢ ‖y‖ * 1 ≤ ‖y‖

Tactic:
mul_one

Goal state after:
case h₂
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
L₁✝ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂✝ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ (E × F)) :=
  LinearMap.mk₂ ℝ (fun x y ↦ (L₁ (x ∘SL inl ℝ E F)) (y ∘SL inl ℝ E F) + (L₂ (x ∘SL inr ℝ E F)) (y ∘SL inr ℝ E F)) ⋯ ⋯ ⋯
    ⋯
x y : StrongDual ℝ (E × F)
⊢ ‖y‖ ≤ ‖y‖
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
⊢ Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑r)) atBot (𝓝 (ρ (⋂ i, s ×ˢ Iic ↑i)))

Tactic:
by
    have h_inter_eq : ⋂ r : ℚ, s ×ˢ Iic ↑(-r) = ⋂ r : ℚ, s ×ˢ Iic (r : ℝ) := by
      ext1 x
      push _ ∈ _
      refine ⟨fun h i ↦ ⟨(h i).1, ?_⟩, fun h i ↦ ⟨(h i).1, ?_⟩⟩ <;> have h' := h (-i)
      · rw [neg_neg] at h'; exact h'.2
      · exact h'.2
    rw [h_inter_eq] at h_neg
    exact tendsto_comp_neg_atTop_iff.mp h_neg

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

Goal state before:
pp: case refine_2
α : 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
⊢ Tendsto (fun i ↦ ∫ (a_1 : β), f (a, a_1) (seq i) ∂ν a) atTop (𝓝 ((ν a).real univ * 1))

Tactic:
mul_one

Goal state after:
case refine_2
α : 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
⊢ Tendsto (fun i ↦ ∫ (a_1 : β), f (a, a_1) (seq i) ∂ν a) atTop (𝓝 ((ν a).real univ))
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a✝ : Unit
r r' : ℚ
hrr' : r ≤ r'
a : α
h₁ : Monotone fun r ↦ preCDF ρ r a
h₂ : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ (preCDF ρ r a).toReal ≤ (preCDF ρ r' a).toReal

Tactic:
exact ENNReal.toReal_mono ((h₂ _).trans_lt ENNReal.one_lt_top).ne (h₁ hrr')

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
c : ℝ≥0
hc : c ≠ 0
⊢ ∀ᵐ (ω : Ω) ∂P, Continuous fun x ↦ (√↑c)⁻¹ * B (c * x) ω

Tactic:
by
    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:
by
    filter_upwards [hB.cont] with ω h
    fun_prop

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝ : SFinite μ
hκ : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ = ⇑(Kernel.id ∥ₖ κ) ∘ₘ ⇑(Kernel.copy α) ∘ₘ μ

Tactic:
simp [FunLike.coe_zero, hκ]

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 α
ν : Measure β
inst✝² : SFinite μ
inst✝¹ : SFinite ν
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
⊢ (⇑κ ∘ₘ μ).prod ν = ⇑(κ ∥ₖ Kernel.id) ∘ₘ μ.prod ν

Tactic:
have h1 : (κ ∘ₘ μ).prod ν = (ν.prod (κ ∘ₘ μ)).map Prod.swap := by rw [Measure.prod_swap]
  have h2 : (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν) = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
    calc (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν)
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((ν.prod μ).map Prod.swap) := by rw [Measure.prod_swap]
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((Kernel.swap _ _) ∘ₘ (ν.prod μ)) := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
    _ = (Kernel.swap _ _) ∘ₘ ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)) := by
      rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]
    _ = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
  rw [← Measure.prod_comp_right, ← h1] at h2
  exact h2.symm

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 Ω
⊢ (ρCond x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)

Tactic:
have : ρCond x s = ((ρ.fst {x})⁻¹ • ρ).comap (fun (y : Ω) ↦ (x, y)) s := by
    congr 2 with s hs
    simp [IsCondKernel.apply_of_ne_zero_of_measurableSet _ _ hx hs,
      (measurableEmbedding_prodMk_left x).comap_apply, Set.singleton_prod]
  simp [this, (measurableEmbedding_prodMk_left x).comap_apply, Set.singleton_prod]

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 α γ
n : ℕ
s : Set β
hs : MeasurableSet s
⊢ Measurable fun p ↦ (κ p.1) (countablePartitionSet n p.2 ×ˢ s) / (ν p.1) (countablePartitionSet n p.2)

Tactic:
by
  refine Measurable.mono (measurable_densityProcess_countableFiltration_aux κ ν n hs) ?_ le_rfl
  exact sup_le_sup le_rfl (comap_mono ((countableFiltration γ).le _))

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

Goal state before:
pp: case hY
Ω : 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
L : StrongDual ℝ (E × F)
this : (⇑L ∘ fun ω ↦ (X ω, Y ω)) = ⇑(L ∘SL inl ℝ E F) ∘ X + ⇑(L ∘SL inr ℝ E F) ∘ Y
⊢ MemLp (⇑(L ∘SL inr ℝ E F) ∘ Y) 2 P

Tactic:
exact (hXY.snd.map _).memLp_two

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

Goal state before:
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) * 1 = (κ 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 ≠ ∞

Tactic:
mul_one

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 ×ˢ s)

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 ≠ ∞
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: case ht
α : 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_ae : ∀ᵐ (t : β) ∂κ.fst a✝, (a✝, t) ∈ {p | (η p) (range e)ᶜ = 0}
a : β
ha : (η (a✝, a)) (range e)ᶜ = 0
⊢ MeasurableSet (Prod.mk a ⁻¹' t)

Tactic:
exact measurable_prodMk_left ht

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁴ : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ✝ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ✝
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
h1 : const Unit ρ.fst = (const Unit ρ).fst
h2 : prodMkLeft Unit ρ.condKernel = (const Unit ρ).condKernelUnitBorel
⊢ ((const Unit ρ).fst ⊗ₖ (const Unit ρ).condKernelUnitBorel) () = ρ

Tactic:
disintegrate

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁴ : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ✝ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ✝
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
h1 : const Unit ρ.fst = (const Unit ρ).fst
h2 : prodMkLeft Unit ρ.condKernel = (const Unit ρ).condKernelUnitBorel
⊢ (const Unit ρ) () = ρ
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
hba : b ≤ a
⊢ IicProdIoc a b = frestrictLe₂ hba ∘ Prod.fst

Tactic:
by
  ext x i
  simp [IicProdIoc, (mem_Iic.1 i.2).trans hba]

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a : ι
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↑(Set.Ioi a)) → X ↑i)
⊢ (fun x ↦ (fun i ↦ x ↑i, fun i ↦ x ↑i)) ((fun x i ↦ if hi : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩) x) = x

Tactic:
ext i
    · simp [mem_Iic.1 i.2]
    · simp [not_le.2 <| Set.mem_Ioi.1 i.2]

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

Goal state before:
pp: case refine_2
α : 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
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ∞
⊢ ∫ (x : β × Ω) in t ×ˢ univ, f x ∂Measure.map (fun a ↦ (X a, Y a)) μ = ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ

Tactic:
setIntegral_map (ht.prod MeasurableSet.univ) hf_int.1 (hX.aemeasurable.prodMk hY),

Goal state after:
case refine_2
α : 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
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ∞
⊢ ∫ (x : α) in (fun a ↦ (X a, Y a)) ⁻¹' t ×ˢ univ, f (X x, Y x) ∂μ = ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ