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

Goal state before:
pp: case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : ↑(sInf {i | n ≤ i ∧ u i ω ∈ s}) < ↑i
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ j, n ≤ j ∧ u j ω ∈ s
h_le : ↑n ≤ hittingAfter u s n ω
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
norm_cast at h'

Goal state after:
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ j, n ≤ j ∧ u j ω ∈ s
h_le : ↑n ≤ hittingAfter u s n ω
h' : sInf {i | n ≤ i ∧ u i ω ∈ s} < i
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
⊢ m₁ ≤ m₂ → (fun x ↦ hittingBtwn u s n x ω) m₁ ≤ (fun x ↦ hittingBtwn u s n x ω) m₂

Tactic:
hm

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
⊢ (fun x ↦ hittingBtwn u s n x ω) m₁ ≤ (fun x ↦ hittingBtwn u s n x ω) m₂
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n : ι
⊢ ∀ ⦃b : ι⦄, n ≤ b → (fun x ↦ hittingBtwn u s x m) n ≤ (fun x ↦ hittingBtwn u s x m) b

Tactic:
n'

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
⊢ n ≤ n' → (fun x ↦ hittingBtwn u s x m) n ≤ (fun x ↦ hittingBtwn u s x m) n'
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m : ι
⊢ Monotone fun x ↦ hittingBtwn u s x m

Tactic:
by
  intro n n' hnn' ω
  simp only [hittingBtwn]
  split_ifs with h_n h_n' h_n'
  · gcongr
    exacts [⟨n, by simp [mem_lowerBounds]; grind⟩]
  · obtain ⟨t, ht⟩ := h_n
    exact csInf_le_of_le ⟨n, by simp [mem_lowerBounds]; grind⟩ ht ht.1.2
  · have ⟨t, ht⟩ := h_n'
    exact absurd ⟨t, ⟨hnn'.trans ht.1.1, ht.1.2⟩, ht.2⟩ h_n
  · simp

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : ConditionallyCompleteLinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : Countable ι
x✝ : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n : ι
hu : Adapted f u
hs : MeasurableSet s
⊢ IsStoppingTime f (hittingAfter u s n)

Tactic:
by
  intro i
  have h_set_eq_Union : {ω | hittingAfter u s n ω ≤ i} = ⋃ j ∈ Set.Icc n i, u j ⁻¹' s := by
    ext; simp [hittingAfter_le_iff]
  simpa [h_set_eq_Union] using MeasurableSet.iUnion fun j =>
    MeasurableSet.iUnion fun hj => f.mono hj.2 _ ((hu j) hs)

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

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
i : ι
s : Set Ω
h : MeasurableSet s
j : ι
hij : ¬i ≤ j
⊢ MeasurableSet (s ∩ {ω | ↑i ≤ ↑j})

Tactic:
norm_cast
      simp only [hij, Set.ofPred_false, Set.inter_empty, @MeasurableSet.empty _ (f.1 j)]

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 𝒢 μ
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:
rwa [hadd, ENNReal.add_le_add_iff_right ENNReal.ofReal_ne_top] at this

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 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ε • μ {ω | ↑ε ≤ (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 ω},
          stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ) +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε},
          stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ)

Tactic:
gcongr with ω hω

Goal state after:
case h₁
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} ≤
    ENNReal.ofReal
      (∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω},
        stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω ∂μ)

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

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

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

case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω : ω ∈ {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}
⊢ f n ω ≤ stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω
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 : ℕ
ω : Ω
hω : ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε
m : ℕ
⊢ m ∈ Set.Icc 0 n → ↑ε ≤ f m ω → sInf (Set.Icc 0 n ∩ {i | ↑ε ≤ f i ω}) = n

Tactic:
hm

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω : ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε
m : ℕ
hm : m ∈ Set.Icc 0 n
⊢ ↑ε ≤ f m ω → sInf (Set.Icc 0 n ∩ {i | ↑ε ≤ f i ω}) = n
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
⊢ u (min (↑((min (↑i) (σ ω)).untop ?neg✝)) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω

Tactic:
coe_untop,

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
i : ι
ω : Ω
hτ : ¬τ ω = ⊤
hσ : ¬σ ω = ⊤
hστ : ¬σ ω ≤ τ ω
⊢ u (min (min (↑i) (σ ω)) (τ ω)).untopA ω = u (min (↑i) ((σ ⊓ τ) ω)).untopA ω
Module: Mathlib.Probability.Process.Stopping

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

Tactic:
hm

Goal state after:
case inl
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
ω : Ω
h : ↑n ≤ τ ω
m : ι
hm : m ∈ {i ∈ s | i < n}
⊢ {ω | τ ω = ↑m}.indicator (u m) ω = 0
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
⊢ ∀ b ∈ {i ∈ s | i < n}, b ≠ i → {ω | τ ω = ↑b}.indicator (u b) ω = 0

Tactic:
intro b

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
b : ι
⊢ b ∈ {i ∈ s | i < n} → b ≠ i → {ω | τ ω = ↑b}.indicator (u b) ω = 0
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: Ω : Type u_2
s : ℕ → Set Ω
ω : Ω
n : ℕ
x✝¹ : Ω
x✝ : x✝¹ ∈ s (n + 1)
⊢ ‖1‖ ≤ 1

Tactic:
norm_one

Goal state after:
Ω : Type u_2
s : ℕ → Set Ω
ω : Ω
n : ℕ
x✝¹ : Ω
x✝ : x✝¹ ∈ s (n + 1)
⊢ 1 ≤ 1
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x ω : Ω
⊢ ↑n + 1 ≤ τ ω ↔ ↑n < τ ω

Tactic:
cases τ ω with
        | top => simp
        | coe t =>
          simp only [Nat.cast_lt]
          norm_cast

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

Goal state before:
pp: case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp (-t * X ω)) μ
ht_nonneg : 0 ≤ t
⊢ Integrable (fun ω ↦ rexp (t * |X ω|)) μ

Tactic:
exact integrable_exp_mul_abs ht_int_pos ht_int_neg

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
h_re_of_mem :
  ∀ (n : ℕ),
    ∀ t ∈ interior (integrableExpSet X μ),
      (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
h_re :
  ∀ (n : ℕ),
    ∀ᶠ (t' : ℝ) in 𝓝 t,
      (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t' * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t' * X ω) ∂μ
⊢ HasDerivAt (fun x ↦ (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑x * ↑(X ω)) ∂μ).re)
    (∫ (ω : Ω), ↑(X ω) ^ (n + 1) * Complex.exp (↑t * ↑(X ω)) ∂μ).re t

Tactic:
exact (hasDerivAt_integral_pow_mul_exp (by simp [ht]) n).real_of_complex

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᵐ[ℙ] gaussianPDFReal μ v
⊢ ∫ (a : ℝ), gaussianPDFReal μ v a = 1

Tactic:
simp only [gaussianPDFReal,
    integral_const_mul]

Goal state after:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᵐ[ℙ] gaussianPDFReal μ v
⊢ (√(2 * π * ↑v))⁻¹ * ∫ (a : ℝ), rexp (-(a - μ) ^ 2 / (2 * ↑v)) = 1
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : 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
⊢ t ≠ 0

Tactic:
suffices |t| ≠ 0 by simpa

Goal state after:
Ω : 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
⊢ |t| ≠ 0
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case refine_2
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ rexp (-(c⁻¹ * x - μ) ^ 2 / (2 * ↑v)) = rexp (-(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v)))

Tactic:
congr 1
    field

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ (gaussianReal μ v) s = ∫⁻ (x : ℝ) in s, gaussianPDF μ v x

Tactic:
gaussianReal_of_var_ne_zero _ hv,

Goal state after:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ (ℙ.withDensity (gaussianPDF μ v)) s = ∫⁻ (x : ℝ) in s, gaussianPDF μ v x
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 (gaussianReal μ v)) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))

Tactic:
gaussianReal_of_var_ne_zero _ hv,

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 (gaussianPDF μ v))) 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) (gaussianReal μ v)) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))

Tactic:
gaussianReal_of_var_ne_zero _ hv,

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 (gaussianPDF μ v))) s =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (v - l) (u - v) / 2
⊢ 0 < min (v - l) (u - v)

Tactic:
simp [hvlu.1, hvlu.2]

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

Goal state before:
pp: Ω : 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 μ
⊢ 0 < min (v - l) (u - v)

Tactic:
simp [hvlu.1, hvlu.2]

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

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : p = 0
⊢ AEStronglyMeasurable X μ

Tactic:
exact hX.aestronglyMeasurable

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 Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet X μ)}

Tactic:
by
  by_cases h_empty : interior (integrableExpSet X μ) = ∅
  · simp [h_empty]
  rw [← ne_eq, ← Set.nonempty_iff_ne_empty] at h_empty
  obtain ⟨t, ht⟩ := h_empty
  have hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)} :=
    analyticOnNhd_complexMGF
  have hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')} :=
    analyticOnNhd_complexMGF
  rw [integrableExpSet_eq_of_mgf' hXY hμμ'] at hX ht ⊢
  refine AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq hX hY
    (convex_integrableExpSet.interior.linear_preimage reLm).isPreconnected
    (z₀ := (t : ℂ)) (by simp [ht]) ?_
  have h_real : ∃ᶠ (x : ℝ) in 𝓝[≠] t, complexMGF X μ x = complexMGF Y μ' x := by
    refine .of_forall fun y ↦ ?_
    rw [complexMGF_ofReal, complexMGF_ofReal, hXY]
  rw [frequently_iff_seq_forall] at h_real ⊢
  obtain ⟨xs, hx_tendsto, hx_eq⟩ := h_real
  refine ⟨fun n ↦ xs n, ?_, fun n ↦ ?_⟩
  · rw [tendsto_nhdsWithin_iff] at hx_tendsto ⊢
    constructor
    · rw [tendsto_ofReal_iff]
      exact hx_tendsto.1
    · simpa using hx_tendsto.2
  · simp [hx_eq]

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

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), ∃ m v, Measure.map (⇑L) μ = gaussianReal m v
⊢ IsGaussian μ

Tactic:
refine isGaussian_of_isGaussian_map fun L ↦ ?_

Goal state after:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), ∃ m v, Measure.map (⇑L) μ = gaussianReal m v
L : E →L[ℝ] ℝ
⊢ IsGaussian (Measure.map (⇑L) μ)
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✝ : BorelSpace E
h : ¬MemLp (fun x ↦ x - ∫ (y : E), y ∂μ) 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ((covarianceBilinDual μ) L₁) L₂ = 0

Tactic:
rw [covarianceBilinDual, uncenteredCovarianceBilinDual_of_not_memLp]
  rw [(measurableEmbedding_subRight _).memLp_map_measure_iff]
  exact h

Goal state after:
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✝² : BorelSpace E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ∫ (x : E), L₁ (x - ∫ (x : E), x ∂μ) * L₂ (x - ∫ (x : E), x ∂μ) ∂μ =
    ∫ (x : E), (L₁ x - ∫ (x : E), L₁ x ∂μ) * (L₂ x - ∫ (x : E), L₂ x ∂μ) ∂μ

pp: case h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝³ : NormedSpace ℝ E
inst✝² : BorelSpace E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ MemLp id 2 (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ)

Tactic:
· have hL (L : StrongDual ℝ E) : μ[L] = L (∫ x, x ∂μ) :=
      L.integral_comp_comm (h.integrable (by simp))
    simp [← hL]

Goal state after:
case h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝³ : NormedSpace ℝ E
inst✝² : BorelSpace E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ MemLp id 2 (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ)
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
t : E
⊢ (∫ (x : Fin (finrank ℝ E) → ℝ),
      cexp (∑ i, ↑⟪x i • (stdOrthonormalBasis ℝ E) i, t⟫ * I) ∂Measure.pi fun x ↦ gaussianReal 0 1) =
    cexp (-↑‖t‖ ^ 2 / 2)

Tactic:
exp_sum,

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
t : E
⊢ (∫ (x : Fin (finrank ℝ E) → ℝ),
      ∏ x_1, cexp (↑⟪x x_1 • (stdOrthonormalBasis ℝ E) x_1, t⟫ * I) ∂Measure.pi fun x ↦ gaussianReal 0 1) =
    cexp (-↑‖t‖ ^ 2 / 2)
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ covarianceBilin (stdGaussian E) = innerSL ℝ

Tactic:
refine gaussian_charFun_congr 0 _ ?_ ?_ |>.2.symm
  · exact LinearMap.BilinForm.isPosSemidef_iff.2 isPosSemidef_inner
  · simp [charFun_stdGaussian, neg_div, innerSL_apply_apply ℝ]

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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable ⇑L
this : IsGaussian (Measure.map X P)
⊢ IsGaussian (Measure.map (⇑L) (Measure.map X P))

pp: case hg
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable ⇑L
this : IsGaussian (Measure.map X P)
⊢ AEMeasurable (⇑L) (Measure.map X P)

pp: case hf
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable ⇑L
this : IsGaussian (Measure.map X P)
⊢ AEMeasurable X P

Tactic:
· exact isGaussian_map_of_measurable hL

Goal state after:
case hg
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable ⇑L
this : IsGaussian (Measure.map X P)
⊢ AEMeasurable (⇑L) (Measure.map X P)

case hf
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable ⇑L
this : IsGaussian (Measure.map X P)
⊢ AEMeasurable X P
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
ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
hm : ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν
hv : covarianceBilin μ = covarianceBilin ν
t : E
⊢ charFun μ t = charFun ν t

Tactic:
IsGaussian.charFun_eq',

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
ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
hm : ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν
hv : covarianceBilin μ = covarianceBilin ν
t : E
⊢ cexp (↑⟪t, ∫ (x : E), id x ∂μ⟫ * I - ↑(((covarianceBilin μ) t) t) / 2) =
    cexp (↑⟪t, ∫ (x : E), id x ∂ν⟫ * I - ↑(((covarianceBilin ν) t) t) / 2)