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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ hittingBtwn f (Set.Iic a) (upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) (N₂ + 1) ω ≤ N₂

Tactic:
hittingBtwn_le_iff_of_lt _ (Nat.lt_succ_self _)

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ ∃ j ∈ Set.Icc (upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) N₂, f j ω ∈ Set.Iic a
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun m ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω
x✝ : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
heq : ¬lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
⊢ f (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω)).untopA ω ≤ f (↑N).untopA ω

Tactic:
exact le_trans (stoppedValue_lowerCrossingTime heq) hf

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

Goal state before:
pp: 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 ω) < ↑ε
this : hittingBtwn f {y | ↑ε ≤ y} 0 n ω = n
⊢ f n ω = f (↑n).untopA ω

Tactic:
congr

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 : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
hωb : (upperBounds (Set.range fun n ↦ f n ω)).Nonempty
i : ℕ
hi : hωb.some < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
n : ℕ
⊢ f (↑n).untopA ω = f n ω

Tactic:
congr

Goal state after:
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this : IsProbabilityMeasure μ
⊢ {ω |
      Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑(filtrationOfSet hsm) k] ω) atTop atTop} =ᵐ[μ]
    Set.univ

Tactic:
have : ∀ᵐ ω ∂μ, ∀ n, (μ[(s (n + 1)).indicator (1 : Ω → ℝ) | filtrationOfSet hsm n]) ω = _ :=
    ae_all_iff.2 fun n => hs.condExp_indicator_filtrationOfSet_ae_eq hsm n.lt_succ_self

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = (fun x ↦ μ.real (s (n + 1))) ω
⊢ {ω |
      Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑(filtrationOfSet hsm) k] ω) atTop atTop} =ᵐ[μ]
    Set.univ
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case e'_2.refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
h : ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
⊢ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)

Tactic:
obtain ⟨c, hc⟩ := h

Goal state after:
case e'_2.refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
⊢ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case e'_2.refine_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
h : ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
⊢ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)

Tactic:
obtain ⟨c, hc⟩ := h

Goal state after:
case e'_2.refine_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
c : ℝ
hc : Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
⊢ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
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
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ BddBelow (Set.range fun n ↦ f n ω)

Tactic:
have hbdd' : ∀ᵐ ω ∂μ, ∀ i, |(-f) (i + 1) ω - (-f) i ω| ≤ R := by
    filter_upwards [hbdd] with ω hω i
    simp only [Pi.neg_apply]
    grind

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
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ BddBelow (Set.range fun n ↦ f n ω)
Module: Mathlib.Probability.Moments.Basic

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

Tactic:
h_rec,

Goal state after:
case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
h_int' : ∀ (i : ι), AEStronglyMeasurable (fun ω ↦ rexp (t * X i ω)) μ
⊢ mgf (X i) μ t * ∏ i ∈ s, mgf (X i) μ t = ∏ i ∈ insert i s, mgf (X i) μ t
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: Ω : Type u_2
s : ℕ → Set Ω
⊢ process s 0 = 0

Tactic:
rw [process, Finset.range_zero, Finset.sum_empty]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
⊢ (complexMGF X μ ↑x).re = mgf X μ x

Tactic:
exact re_complexMGF_ofReal x

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

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

Tactic:
congr

Goal state after:
case e_a.e_a
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ (t / p)⁻¹ = p / t

case e_a
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ max (rexp (t / p * x)) (rexp (-t / p * x)) ^ p = max (rexp (t * x)) (rexp (-t * x))
Module: Mathlib.Probability.Moments.IntegrableExpMul

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

Tactic:
congr

Goal state after:
case e_a.e_a.e_a
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ t * p * p⁻¹ = t

case e_a.e_a
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ t * p * p⁻¹ = t
Module: Mathlib.Probability.Moments.MGFAnalytic

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

Tactic:
simp [hasDerivAt_mgf ht]

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

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

Tactic:
congr

Goal state after:
case refine_2.e_a
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)
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|)
ω : Ω
⊢ (p / (|t| - x)) ^ p * rexp (v * X ω + |t| * |X ω|) = |(p / (|t| - x)) ^ p| * rexp (v * X ω + |t| * |X ω|)

Tactic:
congr

Goal state after:
case refine_2.refine_3.e_a
Ω : 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|)
ω : Ω
⊢ (p / (|t| - x)) ^ p = |(p / (|t| - x)) ^ p|
Module: Mathlib.Probability.Moments.MGFAnalytic

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

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

Tactic:
· rw [pow_two, div_mul_eq_div_div, mul_div_assoc, div_self, mul_one]
      exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'

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

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

Tactic:
congr

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

Goal state before:
pp: m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ gaussianReal (L m) ((L 1 ^ 2).toNNReal * v) = gaussianReal (L m) (max (L 1 ^ 2) 0 * ↑v).toNNReal

Tactic:
congr

Goal state after:
case e_v
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ (L 1 ^ 2).toNNReal * v = (max (L 1 ^ 2) 0 * ↑v).toNNReal
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: case e_v
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ (L 1 ^ 2).toNNReal * v = (max (L 1 ^ 2) 0).toNNReal * v

Tactic:
congr

Goal state after:
case e_v.e_a
m : ℝ
v : ℝ≥0
L : StrongDual ℝ ℝ
⊢ L 1 ^ 2 = max (L 1 ^ 2) 0
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ ∫ (ω : Ω), X ω ^ 2 * rexp (v * X ω) ∂μ - (2 * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      deriv (cgf X μ) v ^ 2 * mgf X μ v =
    ∫ (a : Ω), X a ^ 2 * rexp (v * X a) ∂μ - ∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ +
      ∫ (a : Ω), deriv (cgf X μ) v ^ 2 * rexp (v * X a) ∂μ

Tactic:
congr

Goal state after:
case e_a.e_a.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ (2 * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v =
    ∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ

case e_a.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ deriv (cgf X μ) v ^ 2 * mgf X μ v = ∫ (a : Ω), deriv (cgf X μ) v ^ 2 * rexp (v * X a) ∂μ
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
t : ℝ
⊢ cexp (↑t * I * ↑μ + ↑↑v * (↑t * I) ^ 2 / 2) = cexp (↑t * ↑μ * I - ↑↑v * ↑t ^ 2 / 2)

Tactic:
congr

Goal state after:
μ : ℝ
v : ℝ≥0
t : ℝ
⊢ ↑t * I * ↑μ + ↑↑v * (↑t * I) ^ 2 / 2 = ↑t * ↑μ * I - ↑↑v * ↑t ^ 2 / 2
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✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ cexp (↑(∫ (x : E), L x ∂μ) * I - ↑(max Var[⇑L; μ] 0) / 2) = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)

Tactic:
congr

Goal state after:
case e_a.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ ↑(∫ (x : E), L x ∂μ) = ∫ (x : E), ↑(L x) ∂μ

case e_a.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ max Var[⇑L; μ] 0 = Var[⇑L; μ]
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
this : ⇑L = fun x ↦ L 1 * x
⊢ gaussianReal (L 1 * μ) (NNReal.mk (L 1 ^ 2) ⋯ * v) =
    gaussianReal ((fun x ↦ L 1 * x) μ) (((fun x ↦ L 1 * x) 1 ^ 2).toNNReal * v)

Tactic:
congr

Goal state after:
case e_v.e_a
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
this : ⇑L = fun x ↦ L 1 * x
⊢ L 1 ^ 2 = max ((fun x ↦ L 1 * x) 1 ^ 2) 0
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 μ
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)
L : StrongDual ℝ E
u : ℝ
⊢ cexp ((∫ (x : E), ↑u * ↑(L x) ∂μ) * I - ↑Var[⇑(u • L); μ] / 2) =
    cexp (↑u * ↑(∫ (x : E), L x ∂μ) * I - ↑(max Var[⇑L; μ] 0) * ↑u ^ 2 / 2)

Tactic:
congr

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

case e_a.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)
L : StrongDual ℝ E
u : ℝ
⊢ ↑Var[⇑(u • L); μ] = ↑(max Var[⇑L; μ] 0) * ↑u ^ 2
Module: Mathlib.Probability.Distributions.Gaussian.Basic

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

Tactic:
congr

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
μ✝ : Measure E
inst✝³ : IsGaussian μ✝
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
L : StrongDual ℝ E
this : ∫ (x : E), L x ∂μ ∗ ν = ∫ (x : ℝ), x ∂Measure.map (⇑L) μ ∗ Measure.map (⇑L) ν
⊢ gaussianReal (∫ (x : E), L x ∂μ + ∫ (x : E), L x ∂ν) (Var[⇑L; μ].toNNReal + Var[⇑L; ν].toNNReal) =
    gaussianReal
      (∫ (x : ℝ), x ∂gaussianReal (∫ (x : E), L x ∂μ + ∫ (x : E), L x ∂ν) (Var[⇑L; μ].toNNReal + Var[⇑L; ν].toNNReal))
      Var[id; gaussianReal (∫ (x : E), L x ∂μ + ∫ (x : E), L x ∂ν) (Var[⇑L; μ].toNNReal + Var[⇑L; ν].toNNReal)].toNNReal

Tactic:
congr

Goal state after:
case e_μ
E : Type u_1
F : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
μ✝ : Measure E
inst✝³ : IsGaussian μ✝
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
L : StrongDual ℝ E
this : ∫ (x : E), L x ∂μ ∗ ν = ∫ (x : ℝ), x ∂Measure.map (⇑L) μ ∗ Measure.map (⇑L) ν
⊢ ∫ (x : E), L x ∂μ + ∫ (x : E), L x ∂ν =
    ∫ (x : ℝ), x ∂gaussianReal (∫ (x : E), L x ∂μ + ∫ (x : E), L x ∂ν) (Var[⇑L; μ].toNNReal + Var[⇑L; ν].toNNReal)

case e_v
E : Type u_1
F : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
μ✝ : Measure E
inst✝³ : IsGaussian μ✝
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
L : StrongDual ℝ E
this : ∫ (x : E), L x ∂μ ∗ ν = ∫ (x : ℝ), x ∂Measure.map (⇑L) μ ∗ Measure.map (⇑L) ν
⊢ Var[⇑L; μ].toNNReal + Var[⇑L; ν].toNNReal =
    Var[id; gaussianReal (∫ (x : E), L x ∂μ + ∫ (x : E), L x ∂ν) (Var[⇑L; μ].toNNReal + Var[⇑L; ν].toNNReal)].toNNReal
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
L : StrongDual ℝ E
hL_comp : (⇑L ∘ fun x ↦ x + c) = fun x ↦ L x + L c
⊢ cexp (↑(∫ (x : E), L x ∂μ) * I - ↑Var[⇑L; μ] / 2 + ↑(L c) * I) =
    cexp (↑(∫ (a : E), L a ∂μ + ∫ (a : E), L c ∂μ) * I - ↑Var[⇑L; μ] / 2)

Tactic:
congr

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
L : StrongDual ℝ E
hL_comp : (⇑L ∘ fun x ↦ x + c) = fun x ↦ L x + L c
⊢ ↑(∫ (x : E), L x ∂μ) * I - ↑Var[⇑L; μ] / 2 + ↑(L c) * I =
    ↑(∫ (a : E), L a ∂μ + ∫ (a : E), L c ∂μ) * I - ↑Var[⇑L; μ] / 2