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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k : ℕ
⊢ {i ∈ Finset.range N | i ∈ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)} =
    Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)

Tactic:
ext i
      simp only [Set.mem_Ico, Finset.mem_filter, Finset.mem_range, Finset.mem_Ico,
        and_iff_right_iff_imp, and_imp]
      exact fun _ h => lt_of_lt_of_le h upperCrossingTime_le

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Add ι
inst✝⁴ : LinearOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : Countable ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
ω : Ω
⊢ τ ω + π ω ≤ ↑j ↔ ∃ i, π ω = ↑↑i ∧ τ ω + ↑↑i ≤ ↑j

Tactic:
cases τ ω with
    | top => simp
    | coe a =>
      cases π ω with
      | top => simp
      | coe b => norm_cast; simpa using le_of_add_le_right

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

Goal state before:
pp: case basic
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n ↦ μ[g | ↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n ↦ μ[g | ↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
s✝ : Set Ω
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
s : Set Ω
hs : s ∈ {s | ∃ n, MeasurableSet s}
x✝ : μ s < ∞
⊢ ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ

Tactic:
| basic s hs =>

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

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ eLpNorm (stoppedAbove f r i) 1 μ ≤ ↑(2 * μ Set.univ * ENNReal.ofReal (r + ↑R)).toNNReal

Tactic:
by
  refine (hf.eLpNorm_stoppedAbove_le hr hf0 hbdd i).trans ?_
  simp [ENNReal.coe_toNNReal (measure_ne_top μ _), ENNReal.coe_toNNReal]

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : MeasurableSpace ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : SecondCountableTopology ι
inst✝² : BorelSpace ι
inst✝¹ : TopologicalSpace β
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_meas : IsStronglyProgressive f fun i ω ↦ (min (↑i) (τ ω)).untopA
⊢ IsStronglyProgressive f (MeasureTheory.stoppedProcess u τ)

Tactic:
refine h.comp h_meas fun i ω ↦ ?_

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁸ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : MeasurableSpace ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : SecondCountableTopology ι
inst✝² : BorelSpace ι
inst✝¹ : TopologicalSpace β
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_meas : IsStronglyProgressive f fun i ω ↦ (min (↑i) (τ ω)).untopA
i : ι
ω : Ω
⊢ (min (↑i) (τ ω)).untopA ≤ i
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case inr.h
Ω : 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
⊢ ¬↑n ≤ τ ω

Tactic:
rw [← hi]

Goal state after:
case inr.h
Ω : 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
⊢ ¬↑n ≤ ↑i
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω ↦ rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
⊢ log (mgf (∑ i ∈ s, X i) μ t) = log (∏ i ∈ s, mgf (X i) μ t)

pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω ↦ rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
j : ι
hj : j ∈ s
⊢ mgf (X j) μ t ≠ 0

Tactic:
· rw [h_indep.mgf_sum₀ h_meas]

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω ↦ rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
j : ι
hj : j ∈ s
⊢ mgf (X j) μ t ≠ 0
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝³ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : AddCommMonoid E
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
h : ↑i < ↑n
⊢ ∃ x < n, ↑x = ↑i

Tactic:
exact ⟨i, mod_cast h, rfl⟩

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝² : PartialOrder ι
ℱ : Filtration ι m
inst✝¹ : NormedAddCommGroup E
inst✝ : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ ↑N
⊢ Integrable (stoppedValue u τ) μ

Tactic:
by
  refine integrable_stoppedValue_of_mem_finset hτ hu (s := Finset.Iic N) fun ω => ?_
  simp only [Finset.coe_Iic, Set.mem_image, Set.mem_Iic]
  specialize hbdd ω
  have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at hbdd
  lift τ ω to ι using h_top with i hi
  exact ⟨i, mod_cast hbdd, rfl⟩

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

Goal state before:
pp: case inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ |x| ^ p ≤ (p / -t) ^ p * max (rexp (-t * x)) (rexp (t * x))

Tactic:
convert! rpow_abs_le_mul_max_exp_of_pos x hp (t := -t) (by simp [ht_neg])

Goal state after:
case e'_4
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ t = - -t
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᵐ[ℙ] gaussianPDFReal μ v
⊢ (√(2 * π * ↑v))⁻¹ * ∫ (x : ℝ), rexp (-(↑v)⁻¹ * 2⁻¹ * x ^ 2) = 1

Tactic:
rw [neg_mul, integral_gaussian, ← Real.sqrt_inv, ← Real.sqrt_mul]

Goal state after:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᵐ[ℙ] gaussianPDFReal μ v
⊢ √((2 * π * ↑v)⁻¹ * (π / ((↑v)⁻¹ * 2⁻¹))) = 1

case hx
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᵐ[ℙ] gaussianPDFReal μ v
⊢ 0 ≤ (2 * π * ↑v)⁻¹
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case hx
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᵐ[ℙ] gaussianPDFReal μ v
⊢ 0 ≤ (2 * π * ↑v)⁻¹

Tactic:
· positivity

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

Goal state before:
pp: case refine_5.refine_3
Ω : 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
⊢ 0 ≤ t / 2

pp: case refine_5.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
⊢ t / 2 < |t|

Tactic:
· positivity

Goal state after:
case refine_5.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
⊢ t / 2 < |t|
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
⊢ min (v - l) (u - v) / 2 ≠ 0

pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
⊢ Integrable (fun ω ↦ rexp ((v + min (v - l) (u - v) / 2) * X ω)) μ

pp: case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
⊢ Integrable (fun ω ↦ rexp ((v - min (v - l) (u - v) / 2) * X ω)) μ

Tactic:
· positivity

Goal state after:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
⊢ Integrable (fun ω ↦ rexp ((v + min (v - l) (u - v) / 2) * X ω)) μ

case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
⊢ Integrable (fun ω ↦ rexp ((v - min (v - l) (u - v) / 2) * X ω)) μ
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case neg.refine_1.left
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')}
xs : ℕ → ℝ
hx_tendsto : Tendsto xs atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, xs n ∈ {t}ᶜ
hx_eq : ∀ (n : ℕ), complexMGF X μ ↑(xs n) = complexMGF Y μ' ↑(xs n)
⊢ Tendsto (fun n ↦ ↑(xs n)) atTop (𝓝 ↑t)

pp: case neg.refine_1.right
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')}
xs : ℕ → ℝ
hx_tendsto : Tendsto xs atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, xs n ∈ {t}ᶜ
hx_eq : ∀ (n : ℕ), complexMGF X μ ↑(xs n) = complexMGF Y μ' ↑(xs n)
⊢ ∀ᶠ (n : ℕ) in atTop, ↑(xs n) ∈ {↑t}ᶜ

Tactic:
· rw [tendsto_ofReal_iff]
      exact hx_tendsto.1

Goal state after:
case neg.refine_1.right
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')}
xs : ℕ → ℝ
hx_tendsto : Tendsto xs atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, xs n ∈ {t}ᶜ
hx_eq : ∀ (n : ℕ), complexMGF X μ ↑(xs n) = complexMGF Y μ' ↑(xs n)
⊢ ∀ᶠ (n : ℕ) in atTop, ↑(xs n) ∈ {↑t}ᶜ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω ↦ ↑(X ω ^ p) * cexp (z * ↑(X ω))) μ

Tactic:
by
  have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet hz
  rw [← integrable_norm_iff]
  swap; · fun_prop
  simp only [norm_mul, norm_real, Complex.norm_exp, mul_re, ofReal_re,
    ofReal_im, mul_zero, sub_zero]
  refine (integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet hz hp).mono ?_ ?_
  · fun_prop
  refine ae_of_all _ fun ω ↦ ?_
  simp only [norm_mul, Real.norm_eq_abs, Real.abs_exp]
  gcongr
  exact abs_rpow_le_abs_rpow _ _

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
⊢ IsGaussian μ ↔ ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)

Tactic:
refine ⟨fun h ↦ h.charFunDual_eq, fun h ↦ ⟨fun L ↦ Measure.ext_of_charFun ?_⟩⟩
  ext u
  rw [charFun_map_eq_charFunDual_smul L u, h (u • L), charFun_gaussianReal]
  simp only [smul_apply, smul_eq_mul, ofReal_mul, Real.coe_toNNReal']
  congr
  · rw [integral_const_mul, integral_complex_ofReal]
  · rw [max_eq_left (variance_nonneg _ _), mul_comm, ← ofReal_pow, ← ofReal_mul,
      ← variance_const_mul]
    congr

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

Goal state before:
pp: case hz
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 μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
x : E
⊢ 0 ≤ p.toReal

pp: 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 μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
x : E
⊢ ‖L x‖ₑ ^ p.toReal ≤ (‖L‖ₑ * ‖x‖ₑ) ^ p.toReal

Tactic:
· positivity

Goal state after:
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 μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
x : E
⊢ ‖L x‖ₑ ^ p.toReal ≤ (‖L‖ₑ * ‖x‖ₑ) ^ p.toReal
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: case right
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
n : StrongDual ℝ E → ℤ
h :
  ∀ (L : StrongDual ℝ E),
    ↑(n L) =
      (↑(L (∫ (x : E), id x ∂μ)) * I - ↑(((covarianceBilinDual μ) L) L) / 2 - ↑(L m) * I + ↑((f L) L) / 2) /
        (2 * ↑π * I)
this✝¹ : Continuous n
this✝ : ∀ (x : StrongDual ℝ E), n = Function.const (StrongDual ℝ E) (n x)
this : ∀ (L : StrongDual ℝ E), n L = 0
hn : ∀ (L : StrongDual ℝ E), ((covarianceBilinDual μ) L) L = (f L) L ∧ L (∫ (x : E), x ∂μ) = L m
⊢ f = covarianceBilinDual μ

Tactic:
← toBilinForm_inj

Goal state after:
case right
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
n : StrongDual ℝ E → ℤ
h :
  ∀ (L : StrongDual ℝ E),
    ↑(n L) =
      (↑(L (∫ (x : E), id x ∂μ)) * I - ↑(((covarianceBilinDual μ) L) L) / 2 - ↑(L m) * I + ↑((f L) L) / 2) /
        (2 * ↑π * I)
this✝¹ : Continuous n
this✝ : ∀ (x : StrongDual ℝ E), n = Function.const (StrongDual ℝ E) (n x)
this : ∀ (L : StrongDual ℝ E), n L = 0
hn : ∀ (L : StrongDual ℝ E), ((covarianceBilinDual μ) L) L = (f L) L ∧ L (∫ (x : E), x ∂μ) = L m
⊢ f.toBilinForm = (covarianceBilinDual μ).toBilinForm
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0∞
hp : p ≠ ∞
this : MemLp (fun x ↦ ‖x‖ ^ 2) (p / 2) μ
⊢ MemLp id p μ

Tactic:
← memLp_norm_rpow_iff (q := 2) (by fun_prop) (by simp) (by simp)

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0∞
hp : p ≠ ∞
this : MemLp (fun x ↦ ‖x‖ ^ 2) (p / 2) μ
⊢ MemLp (fun x ↦ ‖id x‖ ^ ENNReal.toReal 2) (p / 2) μ
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

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

Tactic:
rw [add_comm, min_comm]

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X : (t : T) → Ω → 𝓧 t
P : Measure Ω
hX : ∀ (t : T), AEMeasurable (X t) P
I J : Finset T
hJI : J ⊆ I
⊢ (fun I ↦ Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P) J =
    Measure.map (Finset.restrict₂ hJI) ((fun I ↦ Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P) I)

Tactic:
AEMeasurable.map_map_of_aemeasurable (Finset.measurable_restrict₂ _).aemeasurable

Goal state after:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X : (t : T) → Ω → 𝓧 t
P : Measure Ω
hX : ∀ (t : T), AEMeasurable (X t) P
I J : Finset T
hJI : J ⊆ I
⊢ (fun I ↦ Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P) J =
    Measure.map (Finset.restrict₂ hJI ∘ fun ω ↦ I.restrict fun x ↦ X x ω) P

T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X : (t : T) → Ω → 𝓧 t
P : Measure Ω
hX : ∀ (t : T), AEMeasurable (X t) P
I J : Finset T
hJI : J ⊆ I
⊢ AEMeasurable (fun ω ↦ I.restrict fun x ↦ X x ω) P
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case neg
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ¬∃ a, 0 < a ∧ 2⁻¹ < μ {x | ‖x‖ ≤ a} ∧ μ {x | ‖x‖ ≤ a} < 1
b : ℝ
hb : μ {x | ‖x‖ ≤ b} = 1
⊢ ∃ C, 0 < C ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ

Tactic:
have hb' : ∀ᵐ x ∂μ, ‖x‖ ≤ b := by
    rwa [ae_iff_prob_eq_one]
    refine measurable_to_prop ?_
    rw [show (fun x : E ↦ ‖x‖ ≤ b) ⁻¹' {True} = {x : E | ‖x‖ ≤ b} by ext; simp]
    exact measurableSet_le (by fun_prop) (by fun_prop)

Goal state after:
case neg
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ¬∃ a, 0 < a ∧ 2⁻¹ < μ {x | ‖x‖ ≤ a} ∧ μ {x | ‖x‖ ≤ a} < 1
b : ℝ
hb : μ {x | ‖x‖ ≤ b} = 1
hb' : ∀ᵐ (x : E) ∂μ, ‖x‖ ≤ b
⊢ ∃ C, 0 < C ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
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 α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[P] ⇑η
hη✝ : IsMarkovKernel η
π : S → Set (Set Ω) := fun i ↦ {s | ∃ t ∈ squareCylinders fun j ↦ {s | MeasurableSet s}, (fun ω j ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen : ∀ (i : S), MeasurableSpace.comap (fun ω j ↦ X i j ω) MeasurableSpace.pi = generateFrom (π i)
I : Finset S
s : S → Set Ω
J : (i : S) → Finset (T i)
t : (i : S) → (i_1 : T i) → Set (𝓧 i i_1)
ht : ∀ i ∈ I, ∀ (i_1 : T i), MeasurableSet (t i i_1)
hs : ∀ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) = s i
this :
  ⋂ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) =
    ⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j
h' : ∀ i ∈ Finset.univ, MeasurableSet ((↑Finset.univ).pi fun j ↦ t ↑i ↑j)
ω : α
hω :
  (κ ω) (⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j) =
    ∏ i, (κ ω) ((fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j)
hη : κ ω = η ω
⊢ (η ω) (⋂ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i)) =
    ∏ i ∈ I, (η ω) ((fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i))

Tactic:
rw [this, ← hη, hω, ← I.prod_coe_sort]

Goal state after:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[P] ⇑η
hη✝ : IsMarkovKernel η
π : S → Set (Set Ω) := fun i ↦ {s | ∃ t ∈ squareCylinders fun j ↦ {s | MeasurableSet s}, (fun ω j ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen : ∀ (i : S), MeasurableSpace.comap (fun ω j ↦ X i j ω) MeasurableSpace.pi = generateFrom (π i)
I : Finset S
s : S → Set Ω
J : (i : S) → Finset (T i)
t : (i : S) → (i_1 : T i) → Set (𝓧 i i_1)
ht : ∀ i ∈ I, ∀ (i_1 : T i), MeasurableSet (t i i_1)
hs : ∀ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) = s i
this :
  ⋂ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) =
    ⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j
h' : ∀ i ∈ Finset.univ, MeasurableSet ((↑Finset.univ).pi fun j ↦ t ↑i ↑j)
ω : α
hω :
  (κ ω) (⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j) =
    ∏ i, (κ ω) ((fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j)
hη : κ ω = η ω
⊢ ∏ i, (κ ω) ((fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j) =
    ∏ i, (κ ω) ((fun ω j ↦ X (↑i) j ω) ⁻¹' (↑(J ↑i)).pi (t ↑i))
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, Monotone fun r ↦ preCDF ρ r a

Tactic:
Monotone,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, ∀ ⦃a_1 b : ℚ⦄, a_1 ≤ b → preCDF ρ a_1 a ≤ preCDF ρ b a
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ⨅ r, ρ (s ×ˢ Iic ↑↑r) = ρ (s ×ˢ Iic ↑t)

Tactic:
by
  rw [← Monotone.measure_iInter]
  · rw [← prod_iInter]
    congr with x : 1
    simp only [mem_iInter, mem_Iic, Subtype.forall]
    refine ⟨fun h ↦ ?_, fun h a hta ↦ h.trans ?_⟩
    · refine le_of_forall_lt_rat_imp_le fun q htq ↦ h q ?_
      exact mod_cast htq
    · exact mod_cast hta.le
  · exact fun r r' hrr' ↦ prod_mono_right <| by gcongr
  · exact fun _ => (hs.prod measurableSet_Iic).nullMeasurableSet
  · exact ⟨⟨t + 1, lt_add_one _⟩, measure_ne_top ρ _⟩

Goal state after: