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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m_1 x ↦
    match x.1 with
    | 0 => (h₀.approx m_1) x.2
    | n.succ => (⋯.approx m_1) x.2
⊢ IsStronglyPredictable 𝓕 u

Tactic:
let Y m (x : ℕ × Ω) := if x.1 ≤ m then X m x else X m ⟨0, x.2⟩

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m_1 x ↦
    match x.1 with
    | 0 => (h₀.approx m_1) x.2
    | n.succ => (⋯.approx m_1) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
⊢ IsStronglyPredictable 𝓕 u
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
c : ℝ
n : ℕ
⊢ martingalePart (c • f) ℱ μ n =ᵐ[μ] c • martingalePart f ℱ μ n

Tactic:
filter_upwards [predictablePart_smul (f := f) c n] with ω hω
  simpa [martingalePart, smul_sub]

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

Goal state before:
pp: case refine_1
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
⊢ μ[f 0 | ↑ℱ i] =ᵐ[μ] f 0

pp: case refine_2
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
⊢ ∑ i_1 ∈ Finset.range j, μ[f (i_1 + 1) - f i_1 - μ[f (i_1 + 1) - f i_1 | ↑ℱ i_1] | ↑ℱ i] =ᵐ[μ]
    ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])

Tactic:
· rw [condExp_of_stronglyMeasurable (ℱ.le _) _ (hf_int 0)]
      · exact (hf 0).mono (ℱ.mono zero_le)

Goal state after:
case refine_2
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
⊢ ∑ i_1 ∈ Finset.range j, μ[f (i_1 + 1) - f i_1 - μ[f (i_1 + 1) - f i_1 | ↑ℱ i_1] | ↑ℱ i] =ᵐ[μ]
    ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: case pos
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᵐ[μ] μ[f j | ↑ℱ i] - μ[f i | ↑ℱ i]

Tactic:
rw [eventually_sub_nonneg,
    condExp_of_stronglyMeasurable (ℱ.le _) (hf.stronglyAdapted _) (hf.integrable _)]

Goal state after:
case pos
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ f i ≤ᵐ[μ] μ[f j | ↑ℱ i]
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ upperCrossingTime a b f N n ω ≤ N

Tactic:
by
  cases n
  · simp only [upperCrossingTime_zero, Pi.bot_apply, bot_le]
  · simp only [upperCrossingTime_succ, hittingBtwn_le]

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

Goal state before:
pp: case inl
Ω : 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 n' : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
hi : n' ≤ i
h_le : ∀ (ω : Ω), hittingBtwn u s n n' ω ≤ i
⊢ MeasurableSet {ω | (fun ω ↦ ↑(hittingBtwn u s n n' ω)) ω ≤ ↑i}

Tactic:
simp [h_le]

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k : ℕ
⊢ ∑ i ∈ Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω), (f (i + 1) ω - f i ω) =
    stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
      stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω

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

Tactic:
Finset.sum_Ico_eq_add_neg _ lowerCrossingTime_le_upperCrossingTime_succ,

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k : ℕ
⊢ ∑ k ∈ Finset.range (upperCrossingTime a b f N (k + 1) ω), (f (k + 1) ω - f k ω) +
      -∑ k ∈ Finset.range (lowerCrossingTime a b f N k ω), (f (k + 1) ω - f k ω) =
    stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
      stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω

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

Goal state before:
pp: case refine_1
Ω : 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 : ℕ
ω : Ω
⊢ (fun ω ↦ ↑‖f n ω - a‖₊) ω ≤ (fun ω ↦ ↑‖f n ω‖₊ + ↑‖a‖₊) ω

Tactic:
simp_rw [sub_eq_add_neg, ← nnnorm_neg a, ← ENNReal.coe_add, ENNReal.coe_le_coe]

Goal state after:
case refine_1
Ω : 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 : ℕ
ω : Ω
⊢ ‖f n ω + -a‖₊ ≤ ‖f n ω‖₊ + ‖-a‖₊
Module: Mathlib.Probability.Martingale.Convergence

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

Tactic:
posPart_eq_self.2 hnonneg,

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

Goal state before:
pp: case zero
Ω : 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
⊢ upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N 0 = upperCrossingTime a b f N 0 ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N 0 = lowerCrossingTime a b f N 0

Tactic:
refine ⟨rfl, ?_⟩

Goal state after:
case zero
Ω : 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
⊢ lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N 0 = lowerCrossingTime a b f N 0
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
j : WithTop ι
ω : Ω
hxi : τ ω = ↑i
⊢ τ ω ≤ j ↔ ↑i ≤ j

Tactic:
hxi

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
j : WithTop ι
ω : Ω
hxi : τ ω = ↑i
⊢ ↑i ≤ j ↔ ↑i ≤ j
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 : ℕ
x : Ω
hx : ∃ b ∈ range (n + 1), ↑ε ≤ f b x
⊢ ↑ε ≤ stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) x

Tactic:
mem_range,

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
x : Ω
hx : ∃ b < n + 1, ↑ε ≤ f b x
⊢ ↑ε ≤ stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) x
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✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
this : {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ ↑j} = {ω | min (τ ω) ↑j ≤ min (π ω) ↑j} ∩ {ω | τ ω ≤ ↑j}
⊢ MeasurableSet {ω | min (τ ω) ↑j ≤ min (π ω) ↑j}

Tactic:
apply @measurableSet_le _ _ _ _ _ (Filtration.seq f j) _ _ _ _ _ ?_ ?_

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
this : {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ ↑j} = {ω | min (τ ω) ↑j ≤ min (π ω) ↑j} ∩ {ω | τ ω ≤ ↑j}
⊢ Measurable fun a ↦ min (τ a) ↑j

Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
j : ι
this : {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ ↑j} = {ω | min (τ ω) ↑j ≤ min (π ω) ↑j} ∩ {ω | τ ω ≤ ↑j}
⊢ Measurable fun a ↦ min (π a) ↑j
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω ↦ rexp (a * X ω)) μ
hb : Integrable (fun ω ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
| |rexp (a * X ω) + rexp (b * X ω)|

Tactic:
rw [abs_of_nonneg (by positivity)]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω ↦ rexp (a * X ω)) μ
hb : Integrable (fun ω ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
| rexp (a * X ω) + rexp (b * X ω)
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
| |rexp ((v + t) * X ω) + rexp ((v - t) * X ω)|

Tactic:
rw [abs_of_nonneg (by positivity)]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
| rexp ((v + t) * X ω) + rexp ((v - t) * X ω)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
h₁ : τ x = ↑n
h₂ : ↑n + 1 ≤ ↑n
⊢ False

Tactic:
norm_cast at h₂

Goal state after:
case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
h₁ : τ x = ↑n
h₂ : n + 1 ≤ n
⊢ False
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : CompleteSpace E
inst✝⁴ : CompleteSpace F
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
L : E ≃L[𝕜] F
⊢ ∫ (x : F), x ∂Measure.map (⇑L.toHomeomorph.toMeasurableEquiv) μ = L.toHomeomorph.toMeasurableEquiv (∫ (x : E), x ∂μ)

Tactic:
integral_map_equiv

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : CompleteSpace E
inst✝⁴ : CompleteSpace F
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
L : E ≃L[𝕜] F
⊢ ∫ (x : E), L.toHomeomorph.toMeasurableEquiv x ∂μ = L.toHomeomorph.toMeasurableEquiv (∫ (x : E), x ∂μ)
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ ‖∫ (ω : Ω), cexp ((↑z.re + ↑z.im * I) * ↑(X ω)) ∂μ‖ ≤ mgf X μ (↑z.re + ↑z.im * I).re

Tactic:
simp_rw [add_mul, Complex.exp_add, re_add_im]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ ‖∫ (ω : Ω), cexp (↑z.re * ↑(X ω)) * cexp (↑z.im * I * ↑(X ω)) ∂μ‖ ≤ mgf X μ z.re
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ ‖∫ (ω : Ω), cexp (↑z.re * ↑(X ω)) * cexp (↑z.im * I * ↑(X ω)) ∂μ‖ ≤ mgf X μ z.re

Tactic:
calc ‖∫ ω, cexp (z.re * X ω) * cexp (z.im * I * X ω) ∂μ‖
  _ ≤ ∫ ω, ‖cexp (z.re * X ω) * cexp (z.im * I * X ω)‖ ∂μ := norm_integral_le_integral_norm _
  _ = ∫ ω, rexp (z.re * X ω) ∂μ := by simp [Complex.norm_exp]

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 t ↦ ∫ (x : Ω), (fun ω ↦ X ω ^ n * rexp (t * X ω)) x ∂μ)
    (∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t

Tactic:
rw [← EventuallyEq.hasDerivAt_iff (h_re _), ← h_re_of_mem _ t ht]

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

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

Tactic:
integral_sub_right_eq_self (μ := volume) (fun a ↦ rexp (-a ^ 2 / ((2 : ℝ) * v))) μ

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
n : ℕ
⊢ Integrable (fun ω ↦ X ω ^ n * rexp (v * X ω)) μ

Tactic:
by
  convert!
    integrable_rpow_mul_exp_of_integrable_exp_mul ht ht_int_pos ht_int_neg
      (by positivity : 0 ≤ (n : ℝ)) with
    ω
  simp

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

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

Tactic:
rw [add_div, sub_div, sub_add]
    congr 1
    rw [mul_div_cancel_right₀, deriv_cgf h]
    · ring
    · exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module ℝ E
mE : MeasurableSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
mF : MeasurableSpace F
inst✝¹ : OpensMeasurableSpace F
μ : Measure E
L : E →L[ℝ] F
inst✝ : IsGaussian μ
hL : Measurable ⇑L
L' : F →L[ℝ] ℝ
⊢ Measure.map (⇑L' ∘ ⇑L) μ = gaussianReal (∫ (x : E), (L' ∘SL L) x ∂μ) Var[⇑(L' ∘SL L); μ].toNNReal

Tactic:
← ContinuousLinearMap.coe_comp,

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module ℝ E
mE : MeasurableSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
mF : MeasurableSpace F
inst✝¹ : OpensMeasurableSpace F
μ : Measure E
L : E →L[ℝ] F
inst✝ : IsGaussian μ
hL : Measurable ⇑L
L' : F →L[ℝ] ℝ
⊢ Measure.map (⇑(L' ∘SL L)) μ = gaussianReal (∫ (x : E), (L' ∘SL L) x ∂μ) Var[⇑(L' ∘SL L); μ].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 ((∫ (x : E), ↑(L (x + c)) ∂μ) * I - ↑Var[fun x ↦ L x + L c; μ] / 2)

Tactic:
variance_add_const (by fun_prop),

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
⊢ cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2 + ↑(L c) * I) =
    cexp ((∫ (x : E), ↑(L (x + c)) ∂μ) * I - ↑Var[⇑L; μ] / 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
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ 2⁻¹ * |√2| = (√2)⁻¹

Tactic:
rw [abs_of_nonneg (by positivity)]

Goal state after:
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ 2⁻¹ * √2 = (√2)⁻¹
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case neg.inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this✝ : id = fun x ↦ x - c + c
hx : ¬c = 0
I : Integrable (fun x ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (fun x ↦ x - c) (↑p) μ
hp0 : ↑p ≠ 0
this : Integrable (fun x ↦ 2 ^ (↑p).toReal * ‖x - c‖ ^ (↑p).toReal) μ
⊢ |‖c‖ ^ ↑p| ≤ 2 * ‖c‖ ^ (↑p - 1) * ‖y‖ + 2 ^ ↑p * ‖y - c‖ ^ ↑p

Tactic:
rw [abs_of_nonneg (by positivity)]

Goal state after:
case neg.inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this✝ : id = fun x ↦ x - c + c
hx : ¬c = 0
I : Integrable (fun x ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (fun x ↦ x - c) (↑p) μ
hp0 : ↑p ≠ 0
this : Integrable (fun x ↦ 2 ^ (↑p).toReal * ‖x - c‖ ^ (↑p).toReal) μ
⊢ ‖c‖ ^ ↑p ≤ 2 * ‖c‖ ^ (↑p - 1) * ‖y‖ + 2 ^ ↑p * ‖y - c‖ ^ ↑p
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case hx
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 0 < c.toReal / (1 - c).toReal

pp: case hd
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 0 < (1 - d).toReal

pp: case hb
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ d ≠ ∞

pp: case hb
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 1 - c ≠ ∞

Tactic:
· refine div_pos ?_ ?_
    · rw [ENNReal.toReal_pos_iff]
      exact ⟨lt_trans (by norm_num) hc, h.trans_lt (by finiteness)⟩
    · simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt]
      exact ⟨h.trans_lt hd, by finiteness⟩

Goal state after:
case hd
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 0 < (1 - d).toReal

case hb
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ d ≠ ∞

case hb
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 1 - c ≠ ∞
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
inst✝¹ : CompleteSpace E
μ : Measure E
inst✝ : IsGaussian μ
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
⊢ C / 2 < C

Tactic:
simp [hC_pos]

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✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
hC_neg : Integrable (fun x ↦ rexp (-C * ‖x‖ ^ 2)) μ
h_subset : Set.Ioo (-C) C ⊆ interior (integrableExpSet (fun x ↦ ‖x‖ ^ 2) μ)
⊢ -C < 0

Tactic:
simp [hC_pos]

Goal state after: