mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), ⨆ N, ↑(upcrossingsBefore a b f N ω) ∂μ ≤
    ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ

Tactic:
lintegral_iSup'

Goal state after:
case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ENNReal.ofReal (b - a) * ⨆ n, ∫⁻ (a_1 : Ω), ↑(upcrossingsBefore a b f n a_1) ∂μ ≤
    ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ

case pos.hf
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ∀ (n : ℕ), AEMeasurable (fun ω ↦ ↑(upcrossingsBefore a b f n ω)) μ

case pos.h_mono
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ∀ᵐ (x : Ω) ∂μ, Monotone fun n ↦ ↑(upcrossingsBefore a b f n x)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
inst✝ : LinearOrder ι
⊢ (stoppedProcess u fun x ↦ ⊤) = u

Tactic:
by
  ext; simp [stoppedProcess]

Goal state after:
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case neg.refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
h_zero : ¬WithTop.untopA (min (↑i) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i) (leastGE f r ω)) = k + 1
⊢ ↑k < min (↑i) (leastGE f r ω)

Tactic:
have h_top : min (i : ℕ∞) (leastGE f r ω) ≠ ⊤ :=
      ne_top_of_le_ne_top (by simp) (min_le_left _ _)

Goal state after:
case neg.refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
h_zero : ¬WithTop.untopA (min (↑i) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i) (leastGE f r ω)) = k + 1
h_top : min (↑i) (leastGE f r ω) ≠ ⊤
⊢ ↑k < min (↑i) (leastGE f r ω)
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: case ht
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ MeasurableSet {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}

Tactic:
exact measurableSet_lt (measurable_range_sup'' fun n _ =>
          (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)) measurable_const

Goal state after:
Module: Mathlib.Probability.ConditionalExpectation

Goal state before:
pp: case pos.refine_3
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
u v : Ω → E
a✝ : Disjoint (Function.support u) (Function.support v)
huint : MemLp u 1 μ
hvint : MemLp v 1 μ
⊢ StronglyMeasurable u →
    StronglyMeasurable v →
      μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ →
        μ.real s • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ →
          μ.real s • ∫ (x : Ω), (u + v) x ∂μ = ∫ (x : Ω) in s, (u + v) x ∂μ

Tactic:
hu

Goal state after:
case pos.refine_3
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
u v : Ω → E
a✝ : Disjoint (Function.support u) (Function.support v)
huint : MemLp u 1 μ
hvint : MemLp v 1 μ
hu : StronglyMeasurable u
⊢ StronglyMeasurable v →
    μ.real s • ∫ (x : Ω), u x ∂μ = ∫ (x : Ω) in s, u x ∂μ →
      μ.real s • ∫ (x : Ω), v x ∂μ = ∫ (x : Ω) in s, v x ∂μ →
        μ.real s • ∫ (x : Ω), (u + v) x ∂μ = ∫ (x : Ω) in s, (u + v) x ∂μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_1.coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
j : ι
h_set_eq : (fun x ↦ τ (↑x).2) ⁻¹' Set.Iic ↑j = (fun x ↦ (↑x).2) ⁻¹' {ω | τ ω ≤ ↑(min i j)}
⊢ Measurable fun x ↦ (↑x).2

Tactic:
exact measurable_snd.comp (@measurable_subtype_coe _ m_prod _)

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

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ u (↑i).untopA ω = {a | ↑n ≤ τ a}.indicator (u n) ω + {ω | τ ω = ↑i}.indicator (u i) ω

Tactic:
simp only [untopD_coe]

Goal state after:
case inr
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ u i ω = {a | ↑n ≤ τ a}.indicator (u n) ω + {ω | τ ω = ↑i}.indicator (u i) ω
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ t₁ = (a + b) * t₁

Tactic:
hab,

Goal state after:
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ t₁ = 1 * t₁
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ (a + b) * t₂ = t₂

Tactic:
hab,

Goal state after:
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ 1 * t₂ = t₂
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
c : ℝ
hc : 0 < c
⊢ x ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))

Tactic:
refine (h_x_le c hc).trans ?_
      gcongr
      exact le_max_left _ _

Goal state after:
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
u : ℝ
⊢ u ∈ interior (integrableExpSet X μ) → deriv (cgf X μ) u = (∫ (x : Ω), X x * rexp (u * X x) ∂μ) / mgf X μ u

Tactic:
hu

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
u : ℝ
hu : u ∈ interior (integrableExpSet X μ)
⊢ deriv (cgf X μ) u = (∫ (x : Ω), X x * rexp (u * X x) ∂μ) / mgf X μ u
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ (∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
u : ℝ
⊢ u ∈ interior (integrableExpSet X μ) → deriv (mgf X μ) u = ∫ (x : Ω), X x * rexp (u * X x) ∂μ

Tactic:
hu

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ (∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
u : ℝ
hu : u ∈ interior (integrableExpSet X μ)
⊢ deriv (mgf X μ) u = ∫ (x : Ω), X x * rexp (u * X x) ∂μ
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case refine_4
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      ‖↑(X a) ^ (n + 1) * cexp (x * ↑(X a))‖ ≤ |X a| ^ (n + 1) * rexp (z.re * X a + t / 2 * |X a|)

Tactic:
refine ae_of_all _ fun ω ε hε ↦ ?_
    simp only [norm_mul, norm_pow, norm_real, Real.norm_eq_abs]
    rw [Complex.norm_exp]
    simp only [mul_re, ofReal_re, ofReal_im, mul_zero, sub_zero]
    gcongr
    have : ε = z + (ε - z) := by simp
    rw [this, add_re, add_mul]
    gcongr _ + ?_
    refine (le_abs_self _).trans ?_
    rw [abs_mul]
    gcongr
    refine (abs_re_le_norm _).trans ?_
    simp only [Metric.mem_ball, dist_eq_norm] at hε
    exact hε.le

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : v ≠ 0
f : ℝ → ℝ
hf : MeasurableEmbedding f
f' : ℝ → ℝ
h_deriv : ∀ (x : ℝ), HasDerivAt f (f' x) x
s : Set ℝ
hs : MeasurableSet s
⊢ (Measure.comap f (ℙ.withDensity (gaussianPDF μ v))) s =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))

Tactic:
gaussianPDF_def

Goal state after:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
f : ℝ → ℝ
hf : MeasurableEmbedding f
f' : ℝ → ℝ
h_deriv : ∀ (x : ℝ), HasDerivAt f (f' x) x
s : Set ℝ
hs : MeasurableSet s
⊢ (Measure.comap f (ℙ.withDensity fun x ↦ ENNReal.ofReal (gaussianPDFReal μ v x))) s =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : v ≠ 0
f : ℝ ≃ᵐ ℝ
f' : ℝ → ℝ
h_deriv : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x
s : Set ℝ
hs : MeasurableSet s
⊢ (Measure.map (⇑f.symm) (ℙ.withDensity (gaussianPDF μ v))) s =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))

Tactic:
gaussianPDF_def

Goal state after:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
f : ℝ ≃ᵐ ℝ
f' : ℝ → ℝ
h_deriv : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x
s : Set ℝ
hs : MeasurableSet s
⊢ (Measure.map (⇑f.symm) (ℙ.withDensity fun x ↦ ENNReal.ofReal (gaussianPDFReal μ v x))) s =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (complexMGF X μ) (∫ (x : Ω), (fun ω ↦ ↑(X ω) * cexp (z * ↑(X ω))) x ∂μ) z

Tactic:
by
  convert! hasDerivAt_integral_pow_mul_exp hz 0
  · simp [complexMGF]
  · simp

Goal state after:
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst✝ : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
⊢ integrableExpSet X μ = integrableExpSet Y μ'

Tactic:
refine integrableExpSet_eq_of_mgf' hXY ?_

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst✝ : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
⊢ μ = 0 ↔ μ' = 0
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : ¬MemLp id p μ
⊢ ‖(toLpₗ μ p) L‖ ≤ ‖L‖ * (eLpNorm id p μ).toReal

pp: case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
⊢ ‖(toLpₗ μ p) L‖ ≤ ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
· simp only [h_Lp, not_false_eq_true, toLpₗ_of_not_memLp, Lp.norm_zero]
    positivity

Goal state after:
case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
⊢ ‖(toLpₗ μ p) L‖ ≤ ‖L‖ * (eLpNorm id p μ).toReal
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:

Tactic:
‖c‖ ^ (p : ℝ)
    _ ≤ (2 * ‖y - c‖) ^ (p : ℝ) := by
      gcongr
      linarith
    _ = 0 + 2 ^ (p : ℝ) * ‖y - c‖ ^ (p : ℝ) := by
      rw [Real.mul_rpow (by simp) (by positivity)]
      ring
    _ ≤ 2 * ‖c‖ ^ (p - 1 : ℝ) * ‖y‖ + 2 ^ (p : ℝ) * ‖y - c‖ ^ (p : ℝ) := by
      gcongr
      positivity

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

Goal state before:
pp: case e'_3
I : Finset ℝ≥0
s t : ↥I
this : ∀ (s t : ↥I), ↑s ≤ ↑t → ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
hst : ¬↑s ≤ ↑t
⊢ nndist ↑s ↑t = nndist ↑t ↑s

Tactic:
· rw [nndist_comm]

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), AEMeasurable (X i) (⇑κ ∘ₘ P)
hY : AEMeasurable Y (⇑κ ∘ₘ P)
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
⊢ IndepFun (fun ω i ↦ X i ω) Y κ P

Tactic:
refine .congr' ?_ (ae_of_all _ fun _ ↦ .rfl) (Measure.ae_ae_of_ae_comp hY.ae_eq_mk.symm)
  apply process_congr_left (X := fun i ↦ (hX i).mk (X i))
  · refine IndepFun.process_indepFun (fun i ↦ (hX i).measurable_mk) hY.measurable_mk
      fun I ↦ process_congr_left (X := fun (i : I) ↦ X i) ?_ (fun i ↦ ?_)
    · exact (h I).congr' (ae_of_all _ fun _ ↦ .rfl) (Measure.ae_ae_of_ae_comp hY.ae_eq_mk)
    · exact Measure.ae_ae_of_ae_comp (hX i).ae_eq_mk
  exact fun i ↦ Measure.ae_ae_of_ae_comp (hX i).ae_eq_mk.symm

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
⊢ IsPreBrownianReal X P

Tactic:
by
  have h0 : ∀ᵐ ω ∂P, X 0 ω = 0 := by
      apply HasLaw.ae_eq_of_dirac
      rw [← gaussianReal_zero_var]
      exact law 0
  refine IsGaussianProcess.isPreBrownianReal_of_covariance ?_ (fun t ↦ ?_) (fun s t hst ↦ ?_)
  · exact incr.isGaussianProcess (fun t ↦ (law t).hasGaussianLaw) h0
  · rw [(law t).integral_eq, integral_id_gaussianReal]
  have h1 := incr.indepFun_eval_sub zero_le hst h0
  have := (law 0).isProbabilityMeasure
  have h2 : X t = X t - X s + X s := by simp
  rw [h2, covariance_add_right, h1.covariance_eq_zero, covariance_self, (law s).variance_eq,
    variance_id_gaussianReal]
  · simp
  · exact (law s).aemeasurable
  · exact (law s).hasGaussianLaw.memLp_two
  · exact (law t).hasGaussianLaw.memLp_two.sub (law s).hasGaussianLaw.memLp_two
  · exact (law s).hasGaussianLaw.memLp_two
  · exact (law t).hasGaussianLaw.memLp_two.sub (law s).hasGaussianLaw.memLp_two
  · exact (law s).hasGaussianLaw.memLp_two

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 κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ (κ a).real (A ×ˢ Iic ↑q) ≤ ∫ (t : β) in A, ⨅ r, f (a, t) ↑r ∂ν a

Tactic:
rw [← hf.setIntegral a hA]
    refine setIntegral_mono_ae ?_ ?_ ?_
    · exact (hf.integrable _ _).integrableOn
    · exact (hf.integrable_iInf_rat_gt _ _).integrableOn
    · filter_upwards [hf.mono a] with c h_mono using le_ciInf (fun r ↦ h_mono (le_of_lt r.prop))

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

Goal state before:
pp: β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ ((ξ ×ₖ prodMkLeft β η ∘ₖ (κ ×ₖ deterministic f hf)) ω) s =
    ∫⁻ (b : δ), ((η ∘ₖ deterministic f hf) ω) (Prod.mk b ⁻¹' s) ∂(ξ ∘ₖ (κ ×ₖ deterministic f hf)) ω

Tactic:
comp_apply' _ _ _ hs,

Goal state after:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ ∫⁻ (b : β × ε), ((ξ ×ₖ prodMkLeft β η) b) s ∂(κ ×ₖ deterministic f hf) ω =
    ∫⁻ (b : δ), ((η ∘ₖ deterministic f hf) ω) (Prod.mk b ⁻¹' s) ∂(ξ ∘ₖ (κ ×ₖ deterministic f hf)) ω
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ ((ξ ×ₖ prodMkRight β η ∘ₖ (deterministic f hf ×ₖ κ)) ω) s =
    ∫⁻ (b : δ), ((η ∘ₖ deterministic f hf) ω) (Prod.mk b ⁻¹' s) ∂(ξ ∘ₖ (deterministic f hf ×ₖ κ)) ω

Tactic:
comp_apply' _ _ _ hs,

Goal state after:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ ∫⁻ (b : ε × β), ((ξ ×ₖ prodMkRight β η) b) s ∂(deterministic f hf ×ₖ κ) ω =
    ∫⁻ (b : δ), ((η ∘ₖ deterministic f hf) ω) (Prod.mk b ⁻¹' s) ∂(ξ ∘ₖ (deterministic f hf ×ₖ κ)) ω
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: case e'_6.e'_2
Ω : 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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
⊢ 1 = Var[X 0; P].toNNReal / NNReal.mk (√Var[X 0; P] ^ 2) ⋯

Tactic:
ext; simp [h]

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

Goal state before:
pp: case refine_2
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun n ↦ Iic ↑(s n)
⊢ ⋂ i, s' i = ∅

Tactic:
ext x
      simp only [mem_iInter, mem_Iic, mem_empty_iff_false, iff_false, not_forall, not_le, s']
      rw [tendsto_atTop_atBot] at hs_tendsto
      have ⟨q, hq⟩ := exists_rat_lt x
      obtain ⟨i, hi⟩ := hs_tendsto q
      refine ⟨i, lt_of_le_of_lt ?_ hq⟩
      exact mod_cast hi i le_rfl

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 ν
a : α
s : Set β
hs : MeasurableSet s
⊢ MemLp (Filtration.limitProcess (fun n x ↦ κ.densityProcess ν n a x s) (countableFiltration γ) (ν a)) 1 (ν a)

Tactic:
by
  refine Submartingale.memLp_limitProcess (martingale_densityProcess hκν a hs).submartingale
    (R := (ν a univ).toNNReal) (fun n ↦ ?_)
  refine (eLpNorm_densityProcess_le hκν n a s).trans_eq ?_
  rw [ENNReal.coe_toNNReal]
  exact measure_ne_top _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
c : Ω
⊢ ⇑(condDistrib (fun x ↦ c) X μ) =ᵐ[Measure.map X μ] ⇑(Kernel.deterministic (fun x ↦ c) ⋯)

Tactic:
have : (fun _ : α ↦ c) = (fun _ : β ↦ c) ∘ X := rfl
  rw [this]
  filter_upwards [condDistrib_comp_self X (measurable_const (a := c))] with b hb
  rw [hb]

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

Goal state before:
pp: case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (X i)
a b c : ι
i : ↥(Ioc a c)
h : ↑i ≤ b
⊢ Measurable fun c_1 ↦ IocProdIoc a b c c_1 i

pp: case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (X i)
a b c : ι
i : ↥(Ioc a c)
h : ¬↑i ≤ b
⊢ Measurable fun c_1 ↦ IocProdIoc a b c c_1 i

Tactic:
· simpa [IocProdIoc, h] using measurable_fst.eval

Goal state after:
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (X i)
a b c : ι
i : ↥(Ioc a c)
h : ¬↑i ≤ b
⊢ Measurable fun c_1 ↦ IocProdIoc a b c c_1 i
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
a : ℕ
⊢ partialTraj κ a a = Kernel.id

Tactic:
rw [partialTraj_le le_rfl]; rfl

Goal state after: