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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
h_freq : ∃ᶠ (x : ι) in 𝓝[>] t, t < x
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
right✝ : ∀ᶠ (n : ℕ) in atTop, s n ∈ Set.Ioi t
⊢ ∃ s, (∀ (n : ℕ), t < s n) ∧ Tendsto s atTop (𝓝 t)

Tactic:
exact ⟨s, hs_gt, hs_tendsto⟩

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

Goal state before:
pp: case h₁
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
⊢ BddAbove {n | upperCrossingTime a b f M n ω < M}

pp: case a
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
n : ℕ
⊢ upperCrossingTime a b f N n ω < N → upperCrossingTime a b f M n ω < M

Tactic:
· exact upperCrossingTime_lt_bddAbove hab

Goal state after:
case a
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
n : ℕ
⊢ upperCrossingTime a b f N n ω < N → upperCrossingTime a b f M n ω < M
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : sSup {n | upperCrossingTime a b f N n ω < N} < n
⊢ ¬upperCrossingTime a b f N n ω < N

Tactic:
exact fun h => not_le.2 hn (le_csSup (upperCrossingTime_lt_bddAbove hab) h)

Goal state after:
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
g' : Ω → ℝ := fun ω ↦ if h : ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c) then h.choose else 0
hle : ⨆ n, ↑ℱ n ≤ m0
ω : Ω
hω : ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
⊢ Tendsto (fun n ↦ f n ω) atTop (𝓝 hω.choose)

Tactic:
exact hω.choose_spec

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hunif : UniformIntegrable f 1 μ
⊢ Tendsto (fun n ↦ eLpNorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)

Tactic:
obtain ⟨R, hR⟩ := hunif.2.2
  have hmeas : ∀ n, AEStronglyMeasurable (f n) μ := fun n =>
    ((hf.stronglyMeasurable n).mono (ℱ.le _)).aestronglyMeasurable
  exact tendsto_Lp_finite_of_tendstoInMeasure le_rfl ENNReal.one_ne_top hmeas
    (memLp_limitProcess_of_eLpNorm_bdd hmeas hR) hunif.2.1
    (tendstoInMeasure_of_tendsto_ae hmeas <| hf.ae_tendsto_limitProcess hR)

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

Goal state before:
pp: case neg
Ω : 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
hx_fst_le : ↑(↑ω).1 ≤ i
t : ι
ht : ↑t = τ (↑ω).2
⊢ ↑(↑ω).1 ≤ t

Tactic:
refine hx_fst_le.trans (le_of_lt ?_)

Goal state after:
case neg
Ω : 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
hx_fst_le : ↑(↑ω).1 ≤ i
t : ι
ht : ↑t = τ (↑ω).2
⊢ i < t
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ mgf (id ∘ X) μ t = mgf X μ t

pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * id ω)) (Measure.map X μ)

Tactic:
Function.id_comp

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ mgf X μ t = mgf X μ t

Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * id ω)) (Measure.map X μ)
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✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : AddCommMonoid E
N : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ≤ ↑N
⊢ ∃ x ∈ Set.Iic N, ↑x = ↑i

Tactic:
exact ⟨i, mod_cast hbdd, rfl⟩

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

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
⊢ BddAbove (Set.range fun n ↦ f n ω) ↔ BddBelow (Set.range fun n ↦ f n ω)

Tactic:
rw [hω₁, this, ← hω₂]

Goal state after:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
⊢ BddAbove (Set.range fun n ↦ (-f) n ω) ↔ BddBelow (Set.range fun n ↦ f n ω)
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : 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
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ

Tactic:
wlog! h_le : t₁ ≤ t₂

Goal state after:
case inr
Ω : 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
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} ⦃t₁ : ℝ⦄,
    t₁ ∈ integrableExpSet X μ →
      ∀ ⦃t₂ : ℝ⦄,
        t₂ ∈ integrableExpSet X μ →
          ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → t₁ ≤ t₂ → a • t₁ + b • t₂ ∈ integrableExpSet X μ
h_le : t₂ < t₁
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ

Ω✝ : 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 • t₁ + b • t₂ ∈ integrableExpSet X μ
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
p : ℝ≥0∞
u : ι → Ω → E
inst✝² : PartialOrder ι
ℱ : Filtration ι m
inst✝¹ : NormedAddCommGroup E
inst✝ : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ≤ ↑N
⊢ ∃ x ≤ N, ↑x = ↑i

Tactic:
exact ⟨i, mod_cast hbdd, 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 : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ≤ ↑N
⊢ ∃ x ≤ N, ↑x = ↑i

Tactic:
exact ⟨i, mod_cast hbdd, rfl⟩

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

Goal state before:
pp: case e'_4.e'_5
Ω : 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 μ
a : Ω
this : |t| = |t| - x + x
⊢ |t| - x = ||t| - x|

Tactic:
abs_of_nonneg

Goal state after:
case e'_4.e'_5
Ω : 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 μ
a : Ω
this : |t| = |t| - x + x
⊢ |t| - x = |t| - x

case e'_4.e'_5
Ω : 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 μ
a : Ω
this : |t| = |t| - x + x
⊢ 0 ≤ |t| - x
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case e'_4.e'_6
Ω : 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 μ
a : Ω
this : |t| = |t| - x + x
⊢ |t| - x = ||t| - x|

Tactic:
abs_of_nonneg

Goal state after:
case e'_4.e'_6
Ω : 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 μ
a : Ω
this : |t| = |t| - x + x
⊢ |t| - x = |t| - x

case e'_4.e'_6
Ω : 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 μ
a : Ω
this : |t| = |t| - x + x
⊢ 0 ≤ |t| - x
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case neg
Ω : 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 μ')}
h_real : ∃ᶠ (x : ℝ) in 𝓝[≠] t, complexMGF X μ ↑x = complexMGF Y μ' ↑x
⊢ ∃ᶠ (z : ℂ) in 𝓝[≠] ↑t, complexMGF X μ z = complexMGF Y μ' z

Tactic:
frequently_iff_seq_forall

Goal state after:
case neg
Ω : 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 μ')}
h_real : ∃ ns, Tendsto ns atTop (𝓝[≠] t) ∧ ∀ (n : ℕ), complexMGF X μ ↑(ns n) = complexMGF Y μ' ↑(ns n)
⊢ ∃ ns, Tendsto ns atTop (𝓝[≠] ↑t) ∧ ∀ (n : ℕ), complexMGF X μ (ns n) = complexMGF Y μ' (ns n)
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
θ : ℝ
⊢ Measure.map (⇑(ContinuousLinearMap.rotation θ)) (μ.prod μ) = μ.prod μ

Tactic:
refine Measure.ext_of_charFunDual ?_
  ext L
  simp_rw [charFunDual_map, charFunDual_prod, charFunDual_eq_of_forall_strongDual_eq_zero hμ,
    ← Complex.exp_add]
  rw [← add_div, ← add_div, ← neg_add, ← neg_add]
  congr 3
  norm_cast
  have h1 : (L.comp (.rotation θ)).comp (.inl ℝ E E)
      = Real.cos θ • L.comp (.inl ℝ E E) - Real.sin θ • L.comp (.inr ℝ E E) := by
    ext x
    simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.inl_apply,
      ContinuousLinearMap.rotation_apply, smul_zero, add_zero]
    rw [← L.comp_inl_add_comp_inr]
    simp [-neg_smul, sub_eq_add_neg]
  have h2 : (L.comp (.rotation θ)).comp (.inr ℝ E E)
      = Real.sin θ • L.comp (.inl ℝ E E) + Real.cos θ • L.comp (.inr ℝ E E) := by
    ext x
    simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply,
      ContinuousLinearMap.rotation_apply, smul_zero, zero_add, add_apply, smul_apply,
      ContinuousLinearMap.inl_apply, smul_eq_mul]
    rw [← L.comp_inl_add_comp_inr]
    simp
  rw [h1, h2]
  simp only [FunLike.coe_sub, FunLike.coe_smul,
    FunLike.coe_add]
  rw [variance_sub, variance_smul, variance_add, variance_smul, variance_smul, covariance_smul_left,
    covariance_smul_right, variance_smul, covariance_smul_left, covariance_smul_right]
  · have h := Real.cos_sq_add_sin_sq θ
    grind
  all_goals exact (memLp_dual _ _ _ (by simp)).const_smul _

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 : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
y : E
hy : Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
this : ∀ (x : E), rexp (C' * ‖x‖ ^ 2) ≤ rexp (C / ε * ‖y‖ ^ 2) * rexp (C * ‖x - y‖ ^ 2)
⊢ Integrable (fun x ↦ rexp (C' * ‖x‖ ^ 2)) μ

Tactic:
by
    refine integrable_of_le_of_le (g₁ := 0)
      (g₂ := fun x ↦ rexp (C / ε * ‖y‖ ^ 2) * rexp (C * ‖x - y‖ ^ 2)) (by fun_prop) ?_ ?_
      (integrable_const _) (hy.const_mul _)
    · exact ae_of_all _ fun _ ↦ by positivity
    · exact ae_of_all _ this

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
g : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
  f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
    (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
this✝ : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((g L) L) / 2)
hg : g.toBilinForm.IsPosSemidef
this : m = ∫ (x : E), x ∂μ ∧ g = covarianceBilinDual μ
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilin μ

Tactic:
refine ⟨this.1, ?_⟩

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
g : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
  f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
    (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
this✝ : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((g L) L) / 2)
hg : g.toBilinForm.IsPosSemidef
this : m = ∫ (x : E), x ∂μ ∧ g = covarianceBilinDual μ
⊢ f = covarianceBilin μ
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: S : Type u_1
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : BorelSpace E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SecondCountableTopology E
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : S → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL : ∀ (s : S) (ω : Ω), Y s ω = (L s) ((J s).restrict fun x ↦ X x ω)
c : ℝ
x : ↥(I.biUnion J) → E
⊢ (fun s ↦ (L ↑s) fun t ↦ (c • x) ⟨↑t, ⋯⟩) = (RingHom.id ℝ) c • fun s ↦ (L ↑s) fun t ↦ x ⟨↑t, ⋯⟩

Tactic:
ext; simp [← Pi.smul_def]

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

Goal state before:
pp: case inl
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 μ
c : ℝ≥0∞
hc : c ≤ μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha✝ : 0 ≤ a
ha : a = 0
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c)) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * 2 ^ n))

Tactic:
simp only [ha, inv_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, mul_zero,
      zero_mul, Real.exp_zero, ENNReal.ofReal_one, lintegral_const, measure_univ, mul_one,
      ENNReal.toReal_div, neg_mul]

Goal state after:
case inl
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 μ
c : ℝ≥0∞
hc : c ≤ μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha✝ : 0 ≤ a
ha : a = 0
⊢ 1 ≤
    ENNReal.ofReal (rexp (logRatio c)) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-(2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n)))
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 μ
c : ℝ≥0∞
hc : c ≤ μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha : 0 ≤ a
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c)) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * 2 ^ n))

Tactic:
cases ha.eq_or_lt' with
  | inl ha =>
    simp only [ha, inv_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, mul_zero,
      zero_mul, Real.exp_zero, ENNReal.ofReal_one, lintegral_const, measure_univ, mul_one,
      ENNReal.toReal_div, neg_mul]
    refine le_add_right ?_
    rw [← ENNReal.ofReal_one]
    gcongr
    simp only [Real.one_le_exp_iff]
    exact logRatio_nonneg hc_gt.le (hc.trans prob_le_one)
  | inr ha_pos =>
  refine (lintegral_exp_mul_sq_norm_le_mul h_rot ha_pos hc hc_gt).trans ?_
  conv_rhs => rw [← one_mul (ENNReal.ofReal _ + _)]
  gcongr
  exact prob_le_one

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
f : α → StieltjesFunction ℝ
hf : ∀ (q : ℝ), Measurable fun a ↦ ↑(f a) q
hf_bot : ∀ (a : α), Tendsto (↑(f a)) atBot (𝓝 0)
hf_top : ∀ (a : α), Tendsto (↑(f a)) atTop (𝓝 1)
this : ∀ (a : α), IsProbabilityMeasure (f a).measure
⊢ ∀ (i : ℝ), Measurable fun a ↦ ENNReal.ofReal (↑(f a) i - 0)

Tactic:
sub_zero

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
f : α → StieltjesFunction ℝ
hf : ∀ (q : ℝ), Measurable fun a ↦ ↑(f a) q
hf_bot : ∀ (a : α), Tendsto (↑(f a)) atBot (𝓝 0)
hf_top : ∀ (a : α), Tendsto (↑(f a)) atTop (𝓝 1)
this : ∀ (a : α), IsProbabilityMeasure (f a).measure
⊢ ∀ (i : ℝ), Measurable fun a ↦ ENNReal.ofReal (↑(f a) i)
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
this :
  {a | IsRatStieltjesPoint f a} =
    {a | Monotone (f a)} ∩ {a | Tendsto (f a) atTop (𝓝 1)} ∩ {a | Tendsto (f a) atBot (𝓝 0)} ∩
      {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
⊢ MeasurableSet
    ({a | Monotone (f a)} ∩ {a | Tendsto (f a) atTop (𝓝 1)} ∩ {a | Tendsto (f a) atBot (𝓝 0)} ∩
      {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t})

Tactic:
exact (((h1.inter h2).inter h3).inter h4)

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
⊢ MeasurableSet {a | IsRatStieltjesPoint f a}

Tactic:
have h1 : MeasurableSet {a | Monotone (f a)} := by
    change MeasurableSet {a | ∀ q r (_ : q ≤ r), f a q ≤ f a r}
    simp_rw [Set.ofPred_forall]
    refine MeasurableSet.iInter (fun q ↦ ?_)
    refine MeasurableSet.iInter (fun r ↦ ?_)
    refine MeasurableSet.iInter (fun _ ↦ ?_)
    exact measurableSet_le hf.eval hf.eval
  have h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)} :=
    measurableSet_tendsto _ (fun q ↦ hf.eval)
  have h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)} :=
    measurableSet_tendsto _ (fun q ↦ hf.eval)
  have h4 : MeasurableSet {a | ∀ t : ℚ, ⨅ r : Ioi t, f a r = f a t} := by
    rw [Set.ofPred_forall]
    refine MeasurableSet.iInter (fun q ↦ ?_)
    exact measurableSet_eq_fun (.iInf fun _ ↦ hf.eval) hf.eval
  suffices {a | IsRatStieltjesPoint f a}
      = ({a | Monotone (f a)} ∩ {a | Tendsto (f a) atTop (𝓝 1)} ∩ {a | Tendsto (f a) atBot (𝓝 0)}
        ∩ {a | ∀ t : ℚ, ⨅ r : Ioi t, f a r = f a t}) by
    rw [this]
    exact (((h1.inter h2).inter h3).inter h4)
  ext a
  simp only [mem_ofPred_eq, mem_inter_iff]
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · exact ⟨⟨⟨h.mono, h.tendsto_atTop_one⟩, h.tendsto_atBot_zero⟩, h.iInf_rat_gt_eq⟩
  · exact ⟨h.1.1.1, h.1.1.2, h.1.2, h.2⟩

Goal state after:
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' }
⊢ ↑(hf.stieltjesFunction a) ↑↑q = f a ↑q

Tactic:
rw [stieltjesFunction_eq]

Goal state after: