mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet {ω | ↑i ≤ τ ω}

Tactic:
have : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ := by
    ext1 ω; simp only [Set.mem_ofPred_eq, Set.mem_compl_iff, not_lt]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | ↑i ≤ τ ω} = {ω | τ ω < ↑i}ᶜ
⊢ MeasurableSet {ω | ↑i ≤ τ ω}
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : upcrossings a b f ω ≠ ∞
⊢ ¬((∃ᶠ (n : ℕ) in atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in atTop, b < f n ω)

Tactic:
rw [← lt_top_iff_ne_top, upcrossings_lt_top_iff] at hω

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
⊢ ¬((∃ᶠ (n : ℕ) in atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in atTop, b < f n ω)
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this : ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ‖f n x‖ₑ ∂μ ≤ ↑R
n : ℕ
⊢ ∫⁻ (a_1 : Ω), ↑‖f n a_1‖₊ + ↑‖a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * μ Set.univ

Tactic:
lintegral_add_right _ measurable_const,

Goal state after:
case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this : ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ‖f n x‖ₑ ∂μ ≤ ↑R
n : ℕ
⊢ ∫⁻ (a : Ω), ↑‖f n a‖₊ ∂μ + ∫⁻ (a_1 : Ω), ↑‖a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * μ Set.univ
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ.trim ⋯, ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)

Tactic:
let := (⨆ n, ℱ n)

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
this : MeasurableSpace Ω := ⨆ n, ↑ℱ n
⊢ ∀ᵐ (ω : Ω) ∂μ.trim ⋯, ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
this : upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ : ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N (k + 1) ω) N, (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ¬∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a

Tactic:
simp_all only [Set.mem_Iic, not_true_eq_false]

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst✝ : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ Submartingale (stoppedProcess f τ) 𝒢 μ

Tactic:
by
  rw [submartingale_iff_expected_stoppedValue_mono]
  · intro σ π hσ hπ hσ_le_π hπ_bdd
    simp_rw [stoppedValue_stoppedProcess]
    obtain ⟨n, hπ_le_n⟩ := hπ_bdd
    have hπ_top ω : π ω ≠ ⊤ := ne_top_of_le_ne_top (by simp) (hπ_le_n ω)
    have hσ_top ω : σ ω ≠ ⊤ := ne_top_of_le_ne_top (hπ_top ω) (hσ_le_π ω)
    simp only [ne_eq, hσ_top, not_false_eq_true, ↓reduceIte, hπ_top, ge_iff_le]
    exact h.expected_stoppedValue_mono (hσ.min hτ) (hπ.min hτ)
      (fun ω => min_le_min (hσ_le_π ω) le_rfl) fun ω => (min_le_left _ _).trans (hπ_le_n ω)
  · exact StronglyAdapted.stoppedProcess_of_discrete h.stronglyAdapted hτ
  · exact fun i =>
      h.integrable_stoppedValue ((isStoppingTime_const _ i).min hτ) fun ω => min_le_left _ _

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

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

Tactic:
intro x hx

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
x : Ω
hx : ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k x
⊢ ↑ε ≤ stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) x
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} +
      ENNReal.ofReal (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
hadd :
  ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω}, f n ω ∂μ) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}, f n ω ∂μ)
⊢ ↑ε * μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} ≤
    ENNReal.ofReal (∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω}, f n ω ∂μ)

Tactic:
hadd,

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} +
      ENNReal.ofReal (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω}, f n ω ∂μ) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}, f n ω ∂μ)
hadd :
  ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω}, f n ω ∂μ) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}, f n ω ∂μ)
⊢ ↑ε * μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} ≤
    ENNReal.ofReal (∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω}, f n ω ∂μ)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_2
Ω : 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
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
ω : ↑sc
⊢ min (↑↑(↑ω).1) (τ (↑ω).2) = ↑↑(↑ω).1

Tactic:
rw [min_eq_left]

Goal state after:
case refine_2
Ω : 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
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
ω : ↑sc
⊢ ↑↑(↑ω).1 ≤ τ (↑ω).2
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
x : Ω
⊢ 0 x ≤ rexp (t * X x)

Tactic:
rw [Pi.zero_apply]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
x : Ω
⊢ 0 ≤ rexp (t * X x)
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: Ω : Type u_2
s : ℕ → Set Ω
ω : Ω
n : ℕ
⊢ |process s (n + 1) ω - process s n ω| ≤ 1

Tactic:
rw [process, process, Finset.sum_apply, Finset.sum_apply,
    Finset.sum_range_succ_sub_sum, ← Real.norm_eq_abs, norm_indicator_eq_indicator_norm]

Goal state after:
Ω : Type u_2
s : ℕ → Set Ω
ω : Ω
n : ℕ
⊢ (s (n + 1)).indicator (fun a ↦ ‖1 a‖) ω ≤ 1
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
h : ¬Integrable (fun ω ↦ rexp (z.re * X ω)) μ
⊢ ∫ (ω : Ω), cexp (z * ↑(X ω)) ∂μ = 0

Tactic:
integral_undef

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
h : ¬Integrable (fun ω ↦ rexp (z.re * X ω)) μ
⊢ 0 = 0

Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
h : ¬Integrable (fun ω ↦ rexp (z.re * X ω)) μ
⊢ ¬Integrable (fun ω ↦ cexp (z * ↑(X ω))) μ
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    t ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (iteratedDeriv (n + 1) (mgf X μ)) (∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1 + 1) * rexp (t * X ω)) x ∂μ) t

Tactic:
rw [iteratedDeriv_succ]

Goal state after:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    t ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (deriv (iteratedDeriv n (mgf X μ))) (∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1 + 1) * rexp (t * X ω)) x ∂μ) t
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    t ∈ interior (integrableExpSet X μ) →
      iteratedDeriv n (mgf X μ) t = ∫ (x : Ω), (fun ω ↦ X ω ^ n * rexp (t * X ω)) x ∂μ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ iteratedDeriv (n + 1) (mgf X μ) t = ∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ

Tactic:
rw [iteratedDeriv_succ]

Goal state after:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    t ∈ interior (integrableExpSet X μ) →
      iteratedDeriv n (mgf X μ) t = ∫ (x : Ω), (fun ω ↦ X ω ^ n * rexp (t * X ω)) x ∂μ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (mgf X μ)) t = ∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case pos
μ : ℝ
v : ℝ≥0
h : v = 0
⊢ (gaussianReal μ v) Set.univ = 1

Tactic:
simp [gaussianReal_of_var_ne_zero, h]

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

Goal state before:
pp: case neg
μ : ℝ
v : ℝ≥0
h : ¬v = 0
⊢ (gaussianReal μ v) Set.univ = 1

Tactic:
simp [gaussianReal_of_var_ne_zero, h]

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

Goal state before:
pp: case refine_2.refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
h_le : ∀ (a : Ω), |X a| ^ p * rexp (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)
ω : Ω
⊢ |(|(|X ω|)|)| ^ p * rexp (v * X ω + x * |X ω|) ≤ |(p / (|t| - x)) ^ p| * rexp (v * X ω + |t| * |X ω|)

Tactic:
abs_abs

Goal state after:
case refine_2.refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
h_le : ∀ (a : Ω), |X a| ^ p * rexp (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)
ω : Ω
⊢ |X ω| ^ p * rexp (v * X ω + x * |X ω|) ≤ |(p / (|t| - x)) ^ p| * rexp (v * X ω + |t| * |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:
convert! hasDerivAt_integral_pow_mul_exp hz 0
  · simp [complexMGF]
  · simp

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

Goal state before:
pp: case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (iteratedDeriv (n + 1) (complexMGF X μ))
    (∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1 + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Tactic:
rw [iteratedDeriv_succ]

Goal state after:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (deriv (iteratedDeriv n (complexMGF X μ)))
    (∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1 + 1) * cexp (z * ↑(X ω))) x ∂μ) z
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      iteratedDeriv n (complexMGF X μ) z = ∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ n * cexp (z * ↑(X ω))) x ∂μ
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ iteratedDeriv (n + 1) (complexMGF X μ) z = ∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ

Tactic:
rw [iteratedDeriv_succ]

Goal state after:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      iteratedDeriv n (complexMGF X μ) z = ∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ n * cexp (z * ↑(X ω))) x ∂μ
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (complexMGF X μ)) z = ∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case right
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v - min (v - l) (u - v) / 2 < u

Tactic:
· calc v - ((v - l) ⊓ (u - v)) / 2
    _ ≤ v := by
      rw [sub_le_iff_le_add]
      exact le_add_of_nonneg_right (by positivity)
    _ < u := hv.2

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (fun ω ↦ X ω ^ n) μ

Tactic:
convert! integrable_pow_mul_exp_of_mem_interior_integrableExpSet h n
  simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
z : ℂ
hX_meas : AEMeasurable X p
⊢ complexMGF X p z = cexp (z * ↑μ + ↑↑v * z ^ 2 / 2)

Tactic:
← complexMGF_id_map hX_meas,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
z : ℂ
hX_meas : AEMeasurable X p
⊢ complexMGF id (Measure.map X p) z = cexp (z * ↑μ + ↑↑v * z ^ 2 / 2)
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x y : ℝ
⊢ ((covarianceBilin μ) x) y = x * y * Var[id; μ]

Tactic:
by
  by_cases h : MemLp id 2 μ
  · simp only [covarianceBilin_apply_eq_cov h, RCLike.inner_apply, conj_trivial, mul_comm]
    rw [covariance_const_mul_left, covariance_const_mul_right, ← mul_assoc,
      covariance_self aemeasurable_id', Function.id_def]
  · simp [h, variance_of_not_memLp, aestronglyMeasurable_id]

Goal state after:
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
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
x : E
⊢ L (Real.cos θ • x, -Real.sin θ • x) =
    (Real.cos θ • L ∘SL ContinuousLinearMap.inl ℝ E E - Real.sin θ • L ∘SL ContinuousLinearMap.inr ℝ E E) x

Tactic:
← L.comp_inl_add_comp_inr

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
x : E
⊢ (L ∘SL ContinuousLinearMap.inl ℝ E E) (Real.cos θ • x, -Real.sin θ • x).1 +
      (L ∘SL ContinuousLinearMap.inr ℝ E E) (Real.cos θ • x, -Real.sin θ • x).2 =
    (Real.cos θ • L ∘SL ContinuousLinearMap.inl ℝ E E - Real.sin θ • L ∘SL ContinuousLinearMap.inr ℝ E E) x
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
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
h1 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E =
    Real.cos θ • L ∘SL ContinuousLinearMap.inl ℝ E E - Real.sin θ • L ∘SL ContinuousLinearMap.inr ℝ E E
x : E
⊢ L (Real.sin θ • x, Real.cos θ • x) = Real.sin θ * L (x, 0) + Real.cos θ * L (0, x)

Tactic:
← L.comp_inl_add_comp_inr

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
h1 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E =
    Real.cos θ • L ∘SL ContinuousLinearMap.inl ℝ E E - Real.sin θ • L ∘SL ContinuousLinearMap.inr ℝ E E
x : E
⊢ (L ∘SL ContinuousLinearMap.inl ℝ E E) (Real.sin θ • x, Real.cos θ • x).1 +
      (L ∘SL ContinuousLinearMap.inr ℝ E E) (Real.sin θ • x, Real.cos θ • x).2 =
    Real.sin θ * L (x, 0) + Real.cos θ * L (0, x)
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ ∫ (x : E), ‖L₁ x‖ * ‖L₂ x‖ ∂μ ≤ ∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ

Tactic:
by
    refine integral_mono_ae ?_ ?_ (ae_of_all _ fun x ↦ ?_)
    · simp_rw [← norm_mul]
      exact (MemLp.integrable_mul (h.continuousLinearMap_comp L₁)
        (h.continuousLinearMap_comp L₂)).norm
    · simp_rw [mul_assoc]
      refine Integrable.const_mul ?_ _
      simp_rw [← mul_assoc, mul_comm _ (‖L₂‖), mul_assoc, ← pow_two]
      refine Integrable.const_mul ?_ _
      exact h.integrable_norm_pow (by simp)
    · simp only
      rw [mul_assoc]
      gcongr
      · exact ContinuousLinearMap.le_opNorm L₁ x
      · exact ContinuousLinearMap.le_opNorm L₂ x

Goal state after:
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✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
C C' : ℝ
hint :
  (∀ᵐ (x : E) ∂μ, Integrable (fun y ↦ rexp (C * ‖x + y‖ ^ 2)) (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)) ∧
    Integrable (fun x ↦ ∫ (y : E), ‖rexp (C * ‖x + y‖ ^ 2)‖ ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ) μ
hC'_pos : 0 < C'
hC'_lt : C' < C
hC : ∀ᵐ (x : E) ∂μ, Integrable (fun y ↦ rexp (C * ‖x + y‖ ^ 2)) (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
⊢ ∀ᵐ (y : E) ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ

Tactic:
simp only [ContinuousLinearEquiv.coe_neg] at hC

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
C C' : ℝ
hint :
  (∀ᵐ (x : E) ∂μ, Integrable (fun y ↦ rexp (C * ‖x + y‖ ^ 2)) (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)) ∧
    Integrable (fun x ↦ ∫ (y : E), ‖rexp (C * ‖x + y‖ ^ 2)‖ ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ) μ
hC'_pos : 0 < C'
hC'_lt : C' < C
hC : ∀ᵐ (x : E) ∂μ, Integrable (fun y ↦ rexp (C * ‖x + y‖ ^ 2)) (Measure.map (-id) μ)
⊢ ∀ᵐ (y : E) ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: 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_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ μ {x | normThreshold a n < ‖x‖} ≤
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (-Real.log (μ {x | ‖x‖ ≤ a} / (1 - μ {x | ‖x‖ ≤ a})).toReal * 2 ^ n))

Tactic:
refine (measure_gt_normThreshold_le_rpow h_rot ha_gt n).trans_eq ?_

Goal state after:
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_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ μ {x | ‖x‖ ≤ a} * ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ n =
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (-Real.log (μ {x | ‖x‖ ≤ a} / (1 - μ {x | ‖x‖ ≤ a})).toReal * 2 ^ n))