mathlib-initiative/mathlib-tactics huggingface dataset:
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 : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) = fun b ↦
    (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal
⊢ ∫⁻ (x_1 : β), ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, x_1)) x) ∂ν a ≠ ∞

Tactic:
rw [lintegral_stieltjesOfMeasurableRat hf]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) = fun b ↦
    (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal
⊢ (κ a) (univ ×ˢ Iic x) ≠ ∞
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
⊢ IsPreBrownianReal (fun t ω ↦ (√↑c)⁻¹ * B (c * t) ω) P

Tactic:
by
  refine IsGaussianProcess.isPreBrownianReal_of_covariance ?_ (fun t ↦ ?_) (fun s t hst ↦ ?_)
  · have this t ω : (√c)⁻¹ * B (c * t) ω = (√c)⁻¹ • ((B ∘ (c * ·)) t ω) := rfl
    simp_rw [this]
    exact (hB.isGaussianProcess.comp_right _).smul _
  · rw [integral_const_mul, hB.integral_eval, mul_zero]
  · rw [covariance_const_mul_left, covariance_const_mul_right, hB.covariance_eval, min_eq_left]
    · simp [field]
    · exact mul_le_mul_right hst c

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ ∀ s ∈ range Iic, Measurable fun a ↦ (condCDF ρ a).measure s

Tactic:
forall_mem_range,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ ∀ (i : ℝ), Measurable fun a ↦ (condCDF ρ a).measure (Iic i)
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
this :
  (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) - (1 + -((↑(√↑n)⁻¹ * ↑t) ^ 2 / 2))) =o[atTop] fun n ↦
    ((√↑n)⁻¹ * t) ^ 2
aux : (fun n ↦ ‖1 / ↑n‖) = fun n ↦ ‖1 / ↑n‖
⊢ (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) - (1 + -↑t ^ 2 / 2 / ↑n)) =o[atTop] fun x ↦ t ^ 2 * (1 / ↑x)

Tactic:
convert! this using 4 with n

Goal state after:
case e'_7
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
this :
  (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) - (1 + -((↑(√↑n)⁻¹ * ↑t) ^ 2 / 2))) =o[atTop] fun n ↦
    ((√↑n)⁻¹ * t) ^ 2
aux : (fun n ↦ ‖1 / ↑n‖) = fun n ↦ ‖1 / ↑n‖
n : ℕ
⊢ -↑t ^ 2 / 2 / ↑n = -((↑(√↑n)⁻¹ * ↑t) ^ 2 / 2)

case e'_8
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
this :
  (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) - (1 + -((↑(√↑n)⁻¹ * ↑t) ^ 2 / 2))) =o[atTop] fun n ↦
    ((√↑n)⁻¹ * t) ^ 2
aux : (fun n ↦ ‖1 / ↑n‖) = fun n ↦ ‖1 / ↑n‖
x✝ : ℕ
⊢ t ^ 2 * (1 / ↑x✝) = ((√↑x✝)⁻¹ * t) ^ 2
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case e_a
Ω : 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
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this✝ : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (∫ (x : E), x ∂Measure.map X P, ∫ (y : F), y ∂Measure.map Y P) =
    (inl ℝ E F) (∫ (x : E), x ∂Measure.map X P) + (inr ℝ E F) (∫ (y : F), y ∂Measure.map Y P)
⊢ charFunDual (Measure.map X P) (L ∘SL inl ℝ E F) =
    cexp
      (↑(L ((inl ℝ E F) (∫ (x : E), x ∂Measure.map X P))) * I -
        ↑(((covarianceBilinDual (Measure.map X P)) (L ∘SL inl ℝ E F)) (L ∘SL inl ℝ E F)) / 2)

pp: case e_a
Ω : 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
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this✝ : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (∫ (x : E), x ∂Measure.map X P, ∫ (y : F), y ∂Measure.map Y P) =
    (inl ℝ E F) (∫ (x : E), x ∂Measure.map X P) + (inr ℝ E F) (∫ (y : F), y ∂Measure.map Y P)
⊢ charFunDual (Measure.map Y P) (L ∘SL inr ℝ E F) =
    cexp
      (↑(L ((inr ℝ E F) (∫ (y : F), y ∂Measure.map Y P))) * I -
        ↑(((covarianceBilinDual (Measure.map Y P)) (L ∘SL inr ℝ E F)) (L ∘SL inr ℝ E F)) / 2)

Tactic:
· rw [hX.isGaussian_map.charFunDual_eq, integral_complex_ofReal, integral_comp_id_comm,
        covarianceBilinDual_self_eq_variance]
      · simp
      · exact hX.isGaussian_map.memLp_two_id
      · exact hX.isGaussian_map.integrable_id

Goal state after:
case e_a
Ω : 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
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this✝ : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (∫ (x : E), x ∂Measure.map X P, ∫ (y : F), y ∂Measure.map Y P) =
    (inl ℝ E F) (∫ (x : E), x ∂Measure.map X P) + (inr ℝ E F) (∫ (y : F), y ∂Measure.map Y P)
⊢ charFunDual (Measure.map Y P) (L ∘SL inr ℝ E F) =
    cexp
      (↑(L ((inr ℝ E F) (∫ (y : F), y ∂Measure.map Y P))) * I -
        ↑(((covarianceBilinDual (Measure.map Y P)) (L ∘SL inr ℝ E F)) (L ∘SL inr ℝ E F)) / 2)
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 (⇑κ ∘ₘ μ))
⊢ ⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap β α) ∘ₘ ν.prod μ = ⇑(Kernel.swap β γ ∘ₖ (Kernel.id ∥ₖ κ)) ∘ₘ ν.prod μ

Tactic:
Kernel.swap_parallelComp

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 (⇑κ ∘ₘ μ))
⊢ ⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap β α) ∘ₘ ν.prod μ = ⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap β α) ∘ₘ ν.prod μ
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: case pos.left
α : 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
⊢ ∀ᵐ (b : β) ∂κ.fst a, (κCond (a, b)) univ ≤ 1

pp: case pos.right
α : 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
⊢ ∀ᵐ (b : β) ∂κ.fst a, 1 ≤ (κCond (a, b)) univ

Tactic:
· rw [ae_le_const_iff_forall_gt_measure_zero]
    intro r hr
    let s := {b | r ≤ κCond (a, b) Set.univ}
    have hs : MeasurableSet s := h_meas measurableSet_Ici
    have h_2_le : s.indicator (fun _ ↦ r) ≤ s.indicator (fun b ↦ (κCond (a, b)) Set.univ) := by
      intro b
      by_cases hbs : b ∈ s
      · simpa [hbs]
      · simp [hbs]
    have : ∫⁻ b, s.indicator (fun _ ↦ r) b ∂(κ.fst a) ≤ κ.fst a s :=
      (lintegral_mono h_2_le).trans_eq (h_eq s hs)
    rw [lintegral_indicator_const hs] at this
    contrapose! this with h_ne_zero
    conv_lhs => rw [← one_mul (κ.fst a s)]
    gcongr
    finiteness

Goal state after:
case pos.right
α : 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
⊢ ∀ᵐ (b : β) ∂κ.fst a, 1 ≤ (κCond (a, b)) univ
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : ↑S ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ ↑S)
u v : ↥S
⊢ u ≠ v → (Disjoint on fun i ↦ ↑i) u v

Tactic:
huv

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : ↑S ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ ↑S)
u v : ↥S
huv : u ≠ v
⊢ (Disjoint on fun i ↦ ↑i) u v
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case refine_2
Ω : 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
hX : (fun ω i ↦ X i ω) = ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω
hY : (fun ω j ↦ Y j ω) = ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
this✝ : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 (ι → ℝ)
y : WithLp 2 (κ → ℝ)
k : ι
x✝¹ : k ∈ univ
l : κ
x✝ : l ∈ univ
⊢ x.ofLp k * (y.ofLp l * cov[X k, Y l; P]) = 0

Tactic:
h,

Goal state after:
case refine_2
Ω : 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
hX : (fun ω i ↦ X i ω) = ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω
hY : (fun ω j ↦ Y j ω) = ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
this✝ : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 (ι → ℝ)
y : WithLp 2 (κ → ℝ)
k : ι
x✝¹ : k ∈ univ
l : κ
x✝ : l ∈ univ
⊢ x.ofLp k * (y.ofLp l * 0) = 0
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case hn
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : ↑S ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ ↑S)
h_disj : Pairwise (Disjoint on fun i ↦ ↑i)
u v : ↑↑S
⊢ u ≠ v → (Disjoint on fun i ↦ ↑i ×ˢ s) u v

Tactic:
huv

Goal state after:
case hn
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : ↑S ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ ↑S)
h_disj : Pairwise (Disjoint on fun i ↦ ↑i)
u v : ↑↑S
huv : u ≠ v
⊢ (Disjoint on fun i ↦ ↑i ×ˢ s) u v
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

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

Tactic:
Measure.map_map measurable_fst h_prod_embed.measurable,

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
a : α
u : Set β
a✝ : MeasurableSet u
⊢ (Measure.map (Prod.fst ∘ Prod.map id e) (κ a)) u = (κ.fst a) u
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
⊢ HasGaussianLaw (Y - X) P

Tactic:
have : IsProbabilityMeasure P := hX.isProbabilityMeasure
  rw [hasGaussianLaw_iff_charFunDual_map_eq (by fun_prop)]
  intro L
  apply mul_left_cancel₀ (a := charFunDual (P.map X) L)
  · simp [hX.charFunDual_map_eq]
  rw [← Pi.mul_apply, ← h.charFunDual_map_add_eq_mul, add_sub_cancel, hX.charFunDual_map_eq,
    ← exp_add, sub_add_sub_comm, ← add_mul, ← ofReal_add, ← integral_add, ← add_div, ← ofReal_add,
    ← IndepFun.variance_add, hY.charFunDual_map_eq]
  · congr with ω <;> simp
  any_goals fun_prop
  · exact (hX.map L).memLp_two
  · rw [map_comp_sub]
    exact (hY.map L).memLp_two.sub (hX.map L).memLp_two
  · exact h.comp (by fun_prop) (by fun_prop)
  · exact (hX.map L).integrable
  · rw [map_comp_sub]
    exact (hY.map L).integrable.sub (hX.map L).integrable

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
x : α
hxuniv : (κ x) univ = (ρ.condKernel x) univ
t : Set ℝ
ht : MeasurableSet t
heq : (κ x) t = (ρ.condKernel x) t
⊢ (κ x) tᶜ = (ρ.condKernel x) tᶜ

Tactic:
rw [measure_compl ht <| measure_ne_top _ _, heq, hxuniv, measure_compl ht <| measure_ne_top _ _]

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

Goal state before:
pp: case h_union
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
x : α
f : ℕ → Set ℝ
hdisj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
heq : ∀ (i : ℕ), (κ x) (f i) = (ρ.condKernel x) (f i)
⊢ (κ x) (⋃ i, f i) = (ρ.condKernel x) (⋃ i, f i)

Tactic:
rw [measure_iUnion hdisj hf, measure_iUnion hdisj hf]

Goal state after:
case h_union
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
x : α
f : ℕ → Set ℝ
hdisj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
heq : ∀ (i : ℕ), (κ x) (f i) = (ρ.condKernel x) (f i)
⊢ ∑' (i : ℕ), (κ x) (f i) = ∑' (i : ℕ), (ρ.condKernel x) (f i)
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
⊢ ∀ᵐ (x : α) ∂ρ'.fst, (κ.map f) x = ρ'.condKernel x

Tactic:
refine eq_condKernel_of_measure_eq_compProd_real (Kernel.map κ f) ?_

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
⊢ ρ' = ρ'.fst ⊗ₘ κ.map f
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case compl
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A✝ : Set γ
this✝ : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
⊢ ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = ((κ a) (univ ×ˢ s)).toReal - ((κ a) (A ×ˢ s)).toReal

Tactic:
eq_tsub_iff_add_eq_of_le,

Goal state after:
case compl
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A✝ : Set γ
this✝ : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
⊢ ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a + ((κ a) (A ×ˢ s)).toReal = ((κ a) (univ ×ˢ s)).toReal

case compl
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A✝ : Set γ
this✝ : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
⊢ ((κ a) (A ×ˢ s)).toReal ≤ ((κ a) (univ ×ˢ s)).toReal
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: case refine_3
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a b)) → X ↑i)
x✝ :
  (∀ (a_1 : ι) (b_1 : a_1 ≤ a), x.1 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩) ∧
    ∀ (a_1 : ι) (b_1 : a < a_1 ∧ a_1 ≤ b), x.2 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩
i : ι
hi : i ≤ b
h1 : ∀ (a_1 : ι) (b_1 : a_1 ≤ a), x.1 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩
h2 : ∀ (a_1 : ι) (b_1 : a < a_1 ∧ a_1 ≤ b), x.2 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩
⊢ (if h : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩) ∈ s ⟨i, ⋯⟩

Tactic:
· split_ifs with hi3
    · exact h1 i hi3
    · exact h2 i ⟨not_le.1 hi3, hi⟩

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

Goal state before:
pp: case hm
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ Antitone fun m ↦ univ ×ˢ seq m

Tactic:
exact antitone_const.set_prod hseq

Goal state after:
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
this : {s | s ⊆ u ∧ s.ncard ∈ {k}}.Finite
s : Set ι
hs : s ⊆ u ∧ s.ncard = k
⊢ ↑p ^ s.ncard * (1 - ↑p) ^ (u \ s).ncard = ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)

Tactic:
Set.ncard_sdiff' hs.1 hu,

Goal state after:
ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
this : {s | s ⊆ u ∧ s.ncard ∈ {k}}.Finite
s : Set ι
hs : s ⊆ u ∧ s.ncard = k
⊢ ↑p ^ s.ncard * (1 - ↑p) ^ (u.ncard - s.ncard) = ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)
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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X ↑i)
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
⊢ (trajContent κ (frestrictLe a x₀)) (cylinder (Iic b) S) =
    lmarginalPartialTraj κ a b ((cylinder (Iic b) S).indicator 1) x₀

Tactic:
by
  rw [trajContent_cylinder mS, ← lintegral_indicator_one mS, lmarginalPartialTraj]
  congr with x
  apply Set.indicator_const_eq_indicator_const
  rw [mem_cylinder]
  congrm (fun i ↦ ?_) ∈ S
  simp [updateFinset, i.2]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case refine_2
ι : 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 ∈ J
⊢ Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    Function.extend Subtype.val (fun i ↦ (μ ↑i) (if h : ↑i ∈ J then s ⟨↑i, h⟩ else Set.univ)) 1 x

Tactic:
Function.extend_val_apply hx,

Goal state after:
case refine_2
ι : 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 ∈ J
⊢ (μ ↑⟨x, hx⟩) (s ⟨x, hx⟩) =
    Function.extend Subtype.val (fun i ↦ (μ ↑i) (if h : ↑i ∈ J then s ⟨↑i, h⟩ else Set.univ)) 1 x