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

Goal state before:
pp: case h₂
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := ⋯
c : ℝ≥0∞ := ⋯
C : ℝ := ⋯
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
ha : ¬μ {x | ‖x‖ ≤ a} = 1
ha_lt : μ {x | ‖x‖ ≤ a} < 1
hc'_lt : c' < 1
h_iUnion : Set.univ = closedBall 0 a ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n)
⊢ ∫⁻ (a : E) in ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n), ENNReal.ofReal (rexp (C * ‖a‖ ^ 2)) ∂μ ≤
    ∑' (i : ℕ), ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ

Tactic:
exact lintegral_iUnion_le _ _

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

Goal state before:
pp: case h₁
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := ⋯
c : ℝ≥0∞ := ⋯
C : ℝ := ⋯
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
ha : ¬μ {x | ‖x‖ ≤ a} = 1
ha_lt : μ {x | ‖x‖ ≤ a} < 1
hc'_lt : c' < 1
h_iUnion : Set.univ = closedBall 0 a ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n)
this :
  ∫⁻ (x : E) in closedBall 0 (t 0) ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ +
      ∑' (i : ℕ), ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ
⊢ ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ c * ENNReal.ofReal (rexp (logRatio c'))

Tactic:
exact ht_int_zero

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
⊢ iIndepFun (fun t ω s ↦ X t s ω) P

Tactic:
have := hX.isProbabilityMeasure
  classical
  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 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)

pp: case 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 ω)
⊢ ↑Var[fun ω ↦ ∑ i, (L ∘SL single ℝ E i) (X i ω); P] / 2 = ∑ x, ↑Var[fun ω ↦ (L ∘SL single ℝ E x) (X x ω); P] / 2

Tactic:
· simp_rw [← Complex.ofReal_sum]
    rw [integral_finsetSum _ fun i _ ↦ ((hX.eval i).map_fun _).integrable.ofReal]

Goal state after:
case 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 ω)
⊢ ↑Var[fun ω ↦ ∑ i, (L ∘SL single ℝ E i) (X i ω); P] / 2 = ∑ x, ↑Var[fun ω ↦ (L ∘SL single ℝ E x) (X x ω); P] / 2
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ (∫⁻ (a : α) in s, preCDF ρ r a ∂ρ.fst).toReal = (ρ.IicSnd ↑r).real s

Tactic:
rw [setLIntegral_preCDF_fst _ _ hs, measureReal_def]

Goal state after:
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
⊢ (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) - (1 + -↑t ^ 2 / 2 / ↑n)) =o[atTop] fun n ↦ 1 / ↑n

Tactic:
have aux : (fun (n : ℕ) ↦ ‖(1 / n : ℂ)‖) = fun (n : ℕ) ↦ ‖(1 / n : ℝ)‖ := by simp

Goal state after:
Ω : 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 n ↦ 1 / ↑n
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 : ℝ
⊢ Tendsto (fun n ↦ (√↑n)⁻¹ * t) atTop (𝓝 0)

Tactic:
rw [← zero_mul t]

Goal state after:
Ω : 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 : ℝ
⊢ Tendsto (fun n ↦ (√↑n)⁻¹ * t) atTop (𝓝 (0 * t))
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : 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'
h0 : ∫ (x : Ω), X 0 x ∂P = 0
h1 : ∫ (x : Ω), (X 0 ^ 2) x ∂P = 1
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
t : ℝ
⊢ Tendsto (fun n ↦ charFun (↑⟨Measure.map (fun ω ↦ (√↑n)⁻¹ * ∑ k ∈ Finset.range n, X k ω) P, ⋯⟩) t) atTop
    (𝓝 (charFun (↑⟨Measure.map Y P', ⋯⟩) t))

Tactic:
hY.map_eq

Goal state after:
Ω : 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'
h0 : ∫ (x : Ω), X 0 x ∂P = 0
h1 : ∫ (x : Ω), (X 0 ^ 2) x ∂P = 1
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
t : ℝ
⊢ Tendsto (fun n ↦ charFun (↑⟨Measure.map (fun ω ↦ (√↑n)⁻¹ * ∑ k ∈ Finset.range n, X k ω) P, ⋯⟩) t) atTop
    (𝓝 (charFun (↑⟨gaussianReal 0 1, ⋯⟩) t))
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})⁻¹ * ∫⁻ (a : α), {x}.indicator (fun x ↦ (ρCond x) s) a ∂ρ.fst

Tactic:
MeasureTheory.lintegral_indicator (measurableSet_singleton x)

Goal state after:
α : 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})⁻¹ * ∫⁻ (a : α) in {x}, (ρCond a) s ∂ρ.fst
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✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
this : (∀ᵐ (b : β) ∂κ.fst a, (κCond (a, b)) univ ≤ 1) ∧ ∀ᵐ (b : β) ∂κ.fst a, 1 ≤ (κCond (a, b)) univ
⊢ ∀ᵐ (b : β) ∂κ.fst a, (κCond (a, b)) univ = 1

Tactic:
by
    filter_upwards [this.1, this.2] with b h1 h2 using le_antisymm h1 h2

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
q r : ℚ
hqr : q ≤ r
c : γ
⊢ ↑q ≤ ↑r

Tactic:
by exact_mod_cast hqr

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 Ω
κ : Kernel Unit (α × ℝ)
inst✝ : IsFiniteKernel κ
⊢ IsMarkovKernel κ.condKernelUnitReal

Tactic:
rw [condKernelUnitReal]

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 Ω
κ : Kernel Unit (α × ℝ)
inst✝ : IsFiniteKernel κ
⊢ IsMarkovKernel (IsCondKernelCDF.toKernel (fun p ↦ condCDF (κ ()) p.2) ⋯)
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 Ω
κ : Kernel Unit (α × ℝ)
inst✝ : IsFiniteKernel κ
⊢ κ.fst ⊗ₖ κ.condKernelUnitReal = κ

Tactic:
rw [condKernelUnitReal, compProd_toKernel]

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 Ω
κ : Kernel Unit (α × ℝ)
inst✝ : IsFiniteKernel κ
⊢ const Unit (κ ()) = κ
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
⊢ AEStronglyMeasurable (fun x ↦ κ.densityProcess ν i a x s) (ν a)

Tactic:
· exact StronglyMeasurable.aestronglyMeasurable
      (stronglyMeasurable_countableFiltration_densityProcess κ ν i a hs)

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 α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s : Set β
⊢ κ.density ν a x s ≤ 1

Tactic:
by
  refine limsup_le_of_le ?_ ?_
  · exact isCoboundedUnder_le_of_le atTop (fun i ↦ densityProcess_nonneg _ _ _ _ _ _)
  · exact Eventually.of_forall (fun n ↦ densityProcess_le_one hκν _ _ _ _)

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ eLpNorm (fun x ↦ κ.density ν a x s) 1 (ν a) < ∞

Tactic:
exact (eLpNorm_density_le hκν a s).trans_lt (measure_lt_top _ _)

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 α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
⊢ ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)

Tactic:
by
  suffices ∫ x in A, density κ ν a x s ∂(ν a) = ∫ x in A, densityProcess κ ν n a x s ∂(ν a) by
    exact this ▸ setIntegral_densityProcess hκν _ _ hs hA
  suffices ∫ x in A, density κ ν a x s ∂(ν a)
      = limsup (fun i ↦ ∫ x in A, densityProcess κ ν i a x s ∂(ν a)) atTop by
    rw [this, ← limsup_const (α := ℕ) (f := atTop) (∫ x in A, densityProcess κ ν n a x s ∂(ν a)),
      limsup_congr]
    simp only [eventually_atTop]
    refine ⟨n, fun m hnm ↦ ?_⟩
    rw [setIntegral_densityProcess_of_le hκν hnm _ hs hA,
      setIntegral_densityProcess hκν _ _ hs hA]
  -- use L1 convergence
  have h := tendsto_setIntegral_densityProcess hκν a hs A
  rw [h.limsup_eq]

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

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

Tactic:
simp [not_le.2 (mem_Ioc.1 i.2).1]

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 b : ι
hab : a ≤ b
⊢ Measurable
    ⇑{ toFun := fun x i ↦ if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩,
        invFun := fun x ↦ (fun i ↦ x ⟨↑i, ⋯⟩, fun i ↦ x ⟨↑i, ⋯⟩), left_inv := ⋯, right_inv := ⋯ }

Tactic:
refine measurable_pi_lambda _ (fun x ↦ ?_)

Goal state after:
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a b : ι
hab : a ≤ b
x : ↥(Iic b)
⊢ Measurable fun c ↦
    { toFun := fun x i ↦ if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩,
        invFun := fun x ↦ (fun i ↦ x ⟨↑i, ⋯⟩, fun i ↦ x ⟨↑i, ⋯⟩), left_inv := ⋯, right_inv := ⋯ }
      c x
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 : α
μ : Measure β
⊢ ∫ (x : β), f x ∂(const α μ) a = ∫ (x : β), f x ∂μ

Tactic:
const_apply

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
a : α
μ : Measure β
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ
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 : α
μ : Measure β
s : Set β
⊢ ∫ (x : β) in s, f x ∂(const α μ) a = ∫ (x : β) in s, f x ∂μ

Tactic:
const_apply

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
a : α
μ : Measure β
s : Set β
⊢ ∫ (x : β) in s, f x ∂μ = ∫ (x : β) in s, f x ∂μ
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel (X × Y) Z
inst✝ : IsSFiniteKernel η
x : X
s : Set (X × Z)
ms : MeasurableSet s
⊢ ∫⁻ (b : Y), ((deterministic Prod.fst ⋯ ×ₖ η) (x, b)) s ∂κ x = ((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ))) x) s

Tactic:
deterministic_prod_apply' _ _ _ ms,

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst✝¹ : IsSFiniteKernel κ
η : Kernel (X × Y) Z
inst✝ : IsSFiniteKernel η
x : X
s : Set (X × Z)
ms : MeasurableSet s
⊢ ∫⁻ (b : Y), (η (x, b)) (Prod.mk x ⁻¹' s) ∂κ x = ((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ))) x) s
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case neg.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : ¬(κ.fst a) (countablePartitionSet n x) = 0
⊢ (κ a) (countablePartitionSet n x ×ˢ univ) ≠ 0 ∨ (κ.fst a) (countablePartitionSet n x) ≠ 0

Tactic:
exact Or.inr h0

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

Goal state before:
pp: case pos
ι : Type u_1
u : Set ι
p : ↑I
inst✝ : Countable ι
i : ι
hi : i ∈ u
⊢ setBer(u, p) ({a | i ∈ a} ∩ {a | i ∉ u}) = 0

pp: case neg
ι : Type u_1
u : Set ι
p : ↑I
inst✝ : Countable ι
i : ι
hi : i ∉ u
⊢ setBer(u, p) ({a | i ∈ a} ∩ {a | i ∉ u}) = 0

Tactic:
· simp [*]

Goal state after:
case neg
ι : Type u_1
u : Set ι
p : ↑I
inst✝ : Countable ι
i : ι
hi : i ∉ u
⊢ setBer(u, p) ({a | i ∈ a} ∩ {a | i ∉ u}) = 0
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) μ
⊢ Integrable (2 * X * μ[X | m]) μ

Tactic:
rw [mul_assoc]

Goal state after:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
⊢ Integrable (2 * (X * μ[X | m])) μ
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) μ
ω : Ω
⊢ μ[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]) ω
⊢ μ[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.WithDensity

Goal state before:
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:
· simp_rw [withDensity_of_not_measurable _ hf]
    rw [zero_add]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n ↦ f n a
h_sum : Summable fun n ↦ f n
a : α
s : Set β
hs : MeasurableSet s
p : α × β
⊢ (∑' (n : ι), f n) p.1 p.2 = (∑' (n : ι), fun p ↦ f n p.1 p.2) p

Tactic:
tsum_apply h_sum,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n ↦ f n a
h_sum : Summable fun n ↦ f n
a : α
s : Set β
hs : MeasurableSet s
p : α × β
⊢ (∑' (i : ι), f i p.1) p.2 = (∑' (n : ι), fun p ↦ f n p.1 p.2) p