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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
h' : ⨅ r, stieltjesFunctionAux f a ↑r = ⨅ r, stieltjesFunctionAux f a ↑↑r
h'' : ⨅ r, stieltjesFunctionAux f a ↑↑r = ⨅ r, f a ↑r
⊢ Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (stieltjesFunctionAux f a x)) ↔
    Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (⨅ r, f a ↑r))

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
h' : ⨅ r, stieltjesFunctionAux f a ↑r = ⨅ r, stieltjesFunctionAux f a ↑↑r
h'' : ⨅ r, stieltjesFunctionAux f a ↑↑r = ⨅ r, f a ↑r
⊢ Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (stieltjesFunctionAux f a x)) ↔
    Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (⨅ r, f a ↑r))
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)
⊢ ‖L₁‖ * ‖x ∘SL inl ℝ E F‖ * ‖y ∘SL inl ℝ E F‖ ≤ ‖L₁‖ * ‖x‖ * ‖y‖

Tactic:
]

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)
⊢ ‖L₁‖ * ‖x ∘SL inl ℝ E F‖ * ‖y ∘SL inl ℝ E F‖ ≤ ‖L₁‖ * ‖x‖ * ‖y‖
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case hv.inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this✝ : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
i j : ↥I
this :
  ∀ (i j : ↥I),
    ↑i ≤ ↑j →
      cov[(fun ω ↦ ω i) ∘ fun ω ↦ I.restrict fun x ↦ X x ω, (fun ω ↦ ω j) ∘ fun ω ↦ I.restrict fun x ↦ X x ω; P] =
        ↑(min ↑i ↑j)
hij : ¬↑i ≤ ↑j
⊢ ↑(min ↑i ↑j) = ↑(min ↑i ↑j)

Tactic:
]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : (ν a).restrict s = 0
q : ℚ
hq : x < ↑q
⊢ ∫ (b : β) in s, f (a, b) q ∂ν a = 0

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : (ν a).restrict s = 0
q : ℚ
hq : x < ↑q
⊢ ∫ (b : β) in s, f (a, b) q ∂ν a = 0
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
h' : ⨅ r, stieltjesFunctionAux f a ↑r = ⨅ r, stieltjesFunctionAux f a ↑↑r
h'' : ⨅ r, stieltjesFunctionAux f a ↑↑r = ⨅ r, f a ↑r
⊢ ⨅ q, f a ↑q = ⨅ r, f a ↑r

Tactic:
]

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
⊢ ⨅ r, ↑(hf.stieltjesFunction a) ↑↑r ≤ 1

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
⊢ ⨅ r, ↑(hf.stieltjesFunction a) ↑↑r ≤ 1
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
i j : ↥I
hij : ↑i ≤ ↑j
⊢ cov[(fun ω ↦ ω i) ∘ fun ω ↦ I.restrict fun x ↦ X x ω, (fun ω ↦ ω j) ∘ fun ω ↦ I.restrict fun x ↦ X x ω; P] = ↑↑i

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
i j : ↥I
hij : ↑i ≤ ↑j
⊢ cov[(fun ω ↦ ω i) ∘ fun ω ↦ I.restrict fun x ↦ X x ω, (fun ω ↦ ω j) ∘ fun ω ↦ I.restrict fun x ↦ X x ω; P] = ↑↑i
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x < ↑q ∧ ↑q < x + 1
qs : ℝ → ℚ := fun x ↦ ⋯.choose
⊢ ∀ (b : ℚ), ∃ i, ∀ a ≤ i, qs a ≤ b

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x < ↑q ∧ ↑q < x + 1
qs : ℝ → ℚ := fun x ↦ ⋯.choose
⊢ ∀ (b : ℚ), ∃ i, ∀ a ≤ i, qs a ≤ b
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
b : β
⊢ (stieltjesOfMeasurableRat f ⋯ (a, b)).measure (Iic x) = (stieltjesOfMeasurableRat f ⋯ (a, b)).measure (⋂ i, Iic ↑↑i)

pp: case e_f.hs
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
b : β
⊢ Monotone fun r ↦ Iic ↑↑r

pp: case e_f.hsm
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
b : β
⊢ ∀ (i : { r' // x < ↑r' }), NullMeasurableSet (Iic ↑↑i) (stieltjesOfMeasurableRat f ⋯ (a, b)).measure

pp: case e_f.hfin
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
b : β
⊢ ∃ i, (stieltjesOfMeasurableRat f ⋯ (a, b)).measure (Iic ↑↑i) ≠ ∞

Tactic:
]

Goal state after:
case e_f
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
b : β
⊢ (stieltjesOfMeasurableRat f ⋯ (a, b)).measure (Iic x) = (stieltjesOfMeasurableRat f ⋯ (a, b)).measure (⋂ i, Iic ↑↑i)

case e_f.hs
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
b : β
⊢ Monotone fun r ↦ Iic ↑↑r

case e_f.hsm
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
b : β
⊢ ∀ (i : { r' // x < ↑r' }), NullMeasurableSet (Iic ↑↑i) (stieltjesOfMeasurableRat f ⋯ (a, b)).measure

case e_f.hfin
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
b : β
⊢ ∃ i, (stieltjesOfMeasurableRat f ⋯ (a, b)).measure (Iic ↑↑i) ≠ ∞
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‖ ≤ ‖x‖

Tactic:
]

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x < ↑q ∧ ↑q < x + 1
qs : ℝ → ℚ := fun x ↦ ⋯.choose
q : ℚ
y : ℝ
hy : y ≤ ↑q - 1
h_le : ↑(qs y) ≤ ↑q
⊢ qs y ≤ q

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x < ↑q ∧ ↑q < x + 1
qs : ℝ → ℚ := fun x ↦ ⋯.choose
q : ℚ
y : ℝ
hy : y ≤ ↑q - 1
h_le : ↑(qs y) ≤ ↑q
⊢ qs y ≤ q
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x < ↑q ∧ ↑q < x + 1
qs : ℝ → ℚ := fun x ↦ ⋯.choose
hqs_tendsto : Tendsto qs atBot atBot
x : ℝ
⊢ ↑(hf.stieltjesFunction a) x ≤ ↑(hf.stieltjesFunction a) ↑(qs x)

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x < ↑q ∧ ↑q < x + 1
qs : ℝ → ℚ := fun x ↦ ⋯.choose
hqs_tendsto : Tendsto qs atBot atBot
x : ℝ
⊢ ↑(hf.stieltjesFunction a) x ≤ ↑(hf.stieltjesFunction a) ↑(qs 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‖ ≤ ‖y‖

Tactic:
]

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x ↦ ⋯.choose
⊢ ∀ (b : ℚ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ qs a

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x ↦ ⋯.choose
⊢ ∀ (b : ℚ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ qs a
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x ↦ ⋯.choose
q : ℚ
y : ℝ
hy : ↑q + 1 ≤ y
h_le : y ≤ ↑(qs y) + 1
⊢ q ≤ qs y

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x ↦ ⋯.choose
q : ℚ
y : ℝ
hy : ↑q + 1 ≤ y
h_le : y ≤ ↑(qs y) + 1
⊢ q ≤ qs y
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)
⊢ ‖L₂‖ * ‖x ∘SL inr ℝ E F‖ * ‖y ∘SL inr ℝ E F‖ ≤ ‖L₂‖ * ‖x‖ * ‖y‖

Tactic:
]

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)
⊢ ‖L₂‖ * ‖x ∘SL inr ℝ E F‖ * ‖y ∘SL inr ℝ E F‖ ≤ ‖L₂‖ * ‖x‖ * ‖y‖
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x ↦ ⋯.choose
hqs_tendsto : Tendsto qs atTop atTop
x : ℝ
⊢ ↑(hf.stieltjesFunction a) ↑(qs x) ≤ ↑(hf.stieltjesFunction a) x

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x ↦ ⋯.choose
hqs_tendsto : Tendsto qs atTop atTop
x : ℝ
⊢ ↑(hf.stieltjesFunction a) ↑(qs x) ≤ ↑(hf.stieltjesFunction a) x
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
⊢ cov[B (t i.succ), B (t j.succ); P] - cov[B (t i.succ), B (t j.castSucc); P] - cov[B (t i.castSucc), B (t j.succ); P] +
      cov[B (t i.castSucc), B (t j.castSucc); P] =
    0

pp: case hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
⊢ MemLp (B (t i.succ)) 2 P

pp: case hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
⊢ MemLp (B (t i.castSucc)) 2 P

pp: case hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
⊢ MemLp (B (t j.succ)) 2 P

pp: case hT
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
⊢ MemLp (B (t j.castSucc)) 2 P

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
⊢ cov[B (t i.succ), B (t j.succ); P] - cov[B (t i.succ), B (t j.castSucc); P] - cov[B (t i.castSucc), B (t j.succ); P] +
      cov[B (t i.castSucc), B (t j.castSucc); P] =
    0

case hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
⊢ MemLp (B (t i.succ)) 2 P

case hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
⊢ MemLp (B (t i.castSucc)) 2 P

case hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
⊢ MemLp (B (t j.succ)) 2 P

case hT
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
⊢ MemLp (B (t j.castSucc)) 2 P
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
a : α
⊢ ⨅ r, ↑(hf.stieltjesFunction a) ↑↑r = ⨅ r, f a ↑r

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
a : α
⊢ ⨅ r, ↑(hf.stieltjesFunction a) ↑↑r = ⨅ r, f a ↑r
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
a : α
q : { r' // x < ↑r' }
⊢ f a ↑q = f a ↑q

Tactic:
]

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
this : (fun a ↦ ↑(hf.stieltjesFunction a) x) = fun a ↦ ⨅ r, f a ↑r
⊢ Measurable fun a ↦ ⨅ r, f a ↑r

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
this : (fun a ↦ ↑(hf.stieltjesFunction a) x) = fun a ↦ ⨅ r, f a ↑r
⊢ Measurable fun a ↦ ⨅ r, f a ↑r
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ (hf.stieltjesFunction a).measure (Iic x) = ENNReal.ofReal (↑(hf.stieltjesFunction a) x - 0)

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ (hf.stieltjesFunction a).measure (Iic x) = ENNReal.ofReal (↑(hf.stieltjesFunction a) x - 0)
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 = ENNReal.ofReal (1 - 0)

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ (hf.stieltjesFunction a).measure univ = ENNReal.ofReal (1 - 0)
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
⊢ cov[B (t i.succ), B (t j.succ); P] - cov[B (t i.succ), B (t j.castSucc); P] - cov[B (t i.castSucc), B (t j.succ); P] +
      cov[B (t i.castSucc), B (t j.castSucc); P] =
    0

Tactic:
hB.covariance_fun_eval

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
⊢ ↑(min (t i.succ) (t j.succ)) - ↑(min (t i.succ) (t j.castSucc)) - ↑(min (t i.castSucc) (t j.succ)) +
      ↑(min (t i.castSucc) (t j.castSucc)) =
    0
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: case e_f.mk
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
a : α
x : ℝ
fst✝ : Unit
b : α
⊢ toRatCDF (fun p ↦ f p.2) (fst✝, b) = toRatCDF (fun p ↦ f p.2) ((), b)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℝ
s : Set α
hs : MeasurableSet s
⊢ ρ (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' Iic r) = ρ (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' Iic r)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑r)) atTop (𝓝 (ρ (⋃ i, s ×ˢ Iic ↑i)))

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑r)) atTop (𝓝 (ρ (⋃ i, s ×ˢ Iic ↑i)))
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
⊢ Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑r)) atBot (𝓝 (ρ (⋂ i, s ×ˢ Iic ↑i)))

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
⊢ Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑r)) atBot (𝓝 (ρ (⋂ i, s ×ˢ Iic ↑i)))
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case neg.hf_int
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a =
    ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a
h_nonempty : Nonempty { r' // x < ↑r' }
b : { r' // x < ↑r' }
⊢ (κ a) (s ×ˢ Iic ↑↑b) ≠ ∞

Tactic:
]

Goal state after:
case neg.hf_int
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a =
    ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a
h_nonempty : Nonempty { r' // x < ↑r' }
b : { r' // x < ↑r' }
⊢ (κ a) (s ×ˢ Iic ↑↑b) ≠ ∞
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: 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[ℝ] ℝ
h₁ : L₁.toBilinForm.IsPosSemidef
h₂ : L₂.toBilinForm.IsPosSemidef
x : StrongDual ℝ (E × F)
⊢ 0 ≤ (L₁.toBilinForm (x ∘SL inl ℝ E F)) (x ∘SL inl ℝ E F) + (L₂.toBilinForm (x ∘SL inr ℝ E F)) (x ∘SL inr ℝ E F)

Tactic:
]

Goal state after:
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[ℝ] ℝ
h₁ : L₁.toBilinForm.IsPosSemidef
h₂ : L₂.toBilinForm.IsPosSemidef
x : StrongDual ℝ (E × F)
⊢ 0 ≤ (L₁.toBilinForm (x ∘SL inl ℝ E F)) (x ∘SL inl ℝ E F) + (L₂.toBilinForm (x ∘SL inr ℝ E F)) (x ∘SL inr ℝ E F)