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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' {⊥} ×ˢ A = ∅

Tactic:
ext p

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
p : ↑(Set.singleton (n + 1)) × Ω
⊢ p ∈ (fun p ↦ (↑p.1, p.2)) ⁻¹' {⊥} ×ˢ A ↔ p ∈ ∅
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A = ∅

Tactic:
ext p

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
p : ↑(Set.singleton (n + 1)) × Ω
⊢ p ∈ (fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A ↔ p ∈ ∅
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A = {⟨n + 1, ⋯⟩} ×ˢ A

Tactic:
ext p

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
p : ↑(Set.singleton (n + 1)) × Ω
⊢ p ∈ (fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A ↔ p ∈ {⟨n + 1, ⋯⟩} ×ˢ A
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case mp.hb
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
⊢ BddBelow (Set.Icc n m ∩ {i | u i ω ∈ s})

pp: case mp.hs
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
⊢ (Set.Icc n m ∩ {i | u i ω ∈ s}).Nonempty

pp: case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : ∃ b ∈ Set.Icc n m ∩ {i | u i ω ∈ s}, b < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
· exact ⟨n, by simp [mem_lowerBounds]; grind⟩

Goal state after:
case mp.hs
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
⊢ (Set.Icc n m ∩ {i | u i ω ∈ s}).Nonempty

case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m i : ι
hi : i ≤ m
h' : ∃ b ∈ Set.Icc n m ∩ {i | u i ω ∈ s}, b < i
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
hni : n < i
h_le : n ≤ hittingBtwn u s n m ω
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case mp.hb
Ω : 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
⊢ BddBelow {i | n ≤ i ∧ u i ω ∈ s}

pp: case mp.hs
Ω : 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
⊢ {i | n ≤ i ∧ u i ω ∈ s}.Nonempty

pp: 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' : ∃ b ∈ {i | n ≤ i ∧ u i ω ∈ s}, b < i
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
· exact ⟨n, by simp [mem_lowerBounds]; grind⟩

Goal state after:
case mp.hs
Ω : 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
⊢ {i | n ≤ i ∧ u i ω ∈ s}.Nonempty

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' : ∃ b ∈ {i | n ≤ i ∧ u i ω ∈ s}, b < i
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case succ
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : hittingBtwn f (Set.Iic a) (upperCrossingTime a b f N (k + 1) ω) N ω < N
h' : upperCrossingTime a b f N (k + 1) ω < N
this : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω
⊢ ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a

Tactic:
hittingBtwn_lt_iff _ le_rfl

Goal state after:
case succ
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : ∃ j ∈ Set.Ico (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
h' : upperCrossingTime a b f N (k + 1) ω < N
this : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω
⊢ ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
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.Ici b) (lowerCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) (N₂ + 1) ω < N₂ + 1

Tactic:
hittingBtwn_lt_iff _ le_rfl

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.Ico (lowerCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) (N₂ + 1), f j ω ∈ Set.Ici b
Module: Mathlib.Probability.Martingale.OptionalStopping

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

Tactic:
exact fun i =>
      h.integrable_stoppedValue ((isStoppingTime_const _ i).min hτ) fun ω => min_le_left _ _

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

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

Tactic:
have h := measurableSet_eq_stopping_time_min hτ hπ

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
⊢ Tendsto (fun n ↦ eLpNorm (μ[g | ↑ℱ n] - μ[g | ⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)

Tactic:
by
  have ht : Tendsto (fun n => eLpNorm (μ[μ[g | ⨆ n, ℱ n] | ℱ n] - μ[g | ⨆ n, ℱ n]) 1 μ)
      atTop (𝓝 0) :=
    integrable_condExp.tendsto_eLpNorm_condExp stronglyMeasurable_condExp
  have heq : ∀ n, ∀ᵐ x ∂μ, (μ[μ[g | ⨆ n, ℱ n] | ℱ n]) x = (μ[g | ℱ n]) x := fun n =>
    condExp_condExp_of_le (le_iSup _ n) (iSup_le fun n => ℱ.le n)
  refine ht.congr fun n => eLpNorm_congr_ae ?_
  filter_upwards [heq n] with x hxeq
  simp only [hxeq, Pi.sub_apply]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_int_X : AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) μ
h_int_Y : AEStronglyMeasurable (fun ω ↦ rexp (t * Y ω)) μ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * (X + Y) ω)) μ

Tactic:
simp_rw [Pi.add_apply, mul_add, exp_add]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_int_X : AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) μ
h_int_Y : AEStronglyMeasurable (fun ω ↦ rexp (t * Y ω)) μ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * X ω) * rexp (t * Y ω)) μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω ↦ rexp (t * Y ω)) μ
⊢ Integrable (fun ω ↦ rexp (t * (X + Y) ω)) μ

Tactic:
simp_rw [Pi.add_apply, mul_add, exp_add]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (fun ω ↦ rexp (t * Y ω)) μ
⊢ Integrable (fun ω ↦ rexp (t * X ω) * rexp (t * Y ω)) μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case inr
Ω : 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
⊢ u i ω = {a | ↑n ≤ τ a}.indicator (u n) ω + {ω | τ ω = ↑i}.indicator (u i) ω

Tactic:
rw [Set.indicator_of_notMem, zero_add, Set.indicator_of_mem] <;> rw [Set.mem_ofPred]

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
⊢ τ ω = ↑i

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
⊢ ¬↑n ≤ τ ω
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ μ.real {ω | X ω ≤ ε} = μ.real {ω | -ε ≤ (-X) ω}

Tactic:
simp only [Pi.neg_apply, neg_le_neg_iff]

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

Goal state before:
pp: case refine_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ Integrable (fun ω ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) μ

pp: case refine_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      HasDerivAt (fun x ↦ ↑(X a) ^ n * cexp (x * ↑(X a))) (↑(X a) ^ (n + 1) * cexp (x * ↑(X a))) x

Tactic:
· refine integrable_pow_abs_mul_exp_add_of_integrable_exp_mul ?_ ?_ ?_ ?_ (t := t) (n + 1)
    · exact h_subset (add_half_inf_sub_mem_Ioo hlu)
    · exact h_subset (sub_half_inf_sub_mem_Ioo hlu)
    · positivity
    · exact lt_of_lt_of_le (by simp [ht]) (le_abs_self _)

Goal state after:
case refine_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      HasDerivAt (fun x ↦ ↑(X a) ^ n * cexp (x * ↑(X a))) (↑(X a) ^ (n + 1) * cexp (x * ↑(X a))) x
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ ∫ (x : ℝ), x ∂gaussianReal μ v = μ

Tactic:
rw [← deriv_mgf_zero (by simp), mgf_fun_id_gaussianReal, _root_.deriv_exp (by fun_prop)]

Goal state after:
μ : ℝ
v : ℝ≥0
⊢ rexp (μ * 0 + ↑v * 0 ^ 2 / 2) * deriv (fun t ↦ μ * t + ↑v * t ^ 2 / 2) 0 = μ
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✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ max Var[⇑L; μ] 0 = Var[⇑L; μ]

Tactic:
· simp only [sup_eq_left]
      exact variance_nonneg _ _

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

Goal state before:
pp: case pos
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
⊢ covarianceBilin (Measure.map (fun x ↦ c + x) μ) = covarianceBilin μ

pp: case neg
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : ¬MemLp id 2 μ
⊢ covarianceBilin (Measure.map (fun x ↦ c + x) μ) = covarianceBilin μ

Tactic:
· ext x y
    have h_Lp : MemLp id 2 (μ.map (fun x ↦ c + x)) :=
      (measurableEmbedding_addLeft _).memLp_map_measure_iff.mpr <| (memLp_const c).add h
    rw [covarianceBilin_apply h_Lp,
      covarianceBilin_apply h, integral_map (by fun_prop) (by fun_prop)]
    congr with z
    rw [integral_map (by fun_prop) h_Lp.1]
    simp only [id_eq]
    rw [integral_add (integrable_const _)]
    · simp
    · exact h.integrable (by simp)

Goal state after:
case neg
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : ¬MemLp id 2 μ
⊢ covarianceBilin (Measure.map (fun x ↦ c + x) μ) = covarianceBilin μ
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
i : ι
x✝¹ : i ∈ Finset.univ
j : ι
x✝ : j ∈ Finset.univ
⊢ cov[fun ω ↦ x.ofLp i * X i ω, fun ω ↦ y.ofLp j * X j ω; μ] = x.ofLp i * y.ofLp j * cov[X i, X j; μ]

Tactic:
rw [covariance_const_mul_left, covariance_const_mul_right]

Goal state after:
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
i : ι
x✝¹ : i ∈ Finset.univ
j : ι
x✝ : j ∈ Finset.univ
⊢ x.ofLp i * (y.ofLp j * cov[X i, X j; μ]) = x.ofLp i * y.ofLp j * cov[X i, X j; μ]
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case hX
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEStronglyMeasurable (fun u ↦ ⟪x, u⟫) (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)

pp: case hY
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEStronglyMeasurable (fun u ↦ ⟪y, u⟫) (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)

pp: case hZ
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEMeasurable (fun ω ↦ toLp 2 fun x ↦ X x ω) μ

pp: case h
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ MemLp id 2 (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)

Tactic:
any_goals exact Measurable.aestronglyMeasurable (by fun_prop)

Goal state after:
case hZ
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEMeasurable (fun ω ↦ toLp 2 fun x ↦ X x ω) μ

case h
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ MemLp id 2 (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)
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✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
h :
  ∀ (L : StrongDual ℝ E),
    cexp (↑(L (∫ (x : E), id x ∂μ)) * I - ↑(((covarianceBilinDual μ) L) L) / 2) = cexp (↑(L m) * I - ↑((f L) L) / 2)
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ

Tactic:
Complex.exp_eq_exp_iff_exists_int

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✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
h :
  ∀ (L : StrongDual ℝ E),
    ∃ n,
      ↑(L (∫ (x : E), id x ∂μ)) * I - ↑(((covarianceBilinDual μ) L) L) / 2 =
        ↑(L m) * I - ↑((f L) L) / 2 + ↑n * (2 * ↑π * I)
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:

Tactic:
∫ x, ∫ y, L x + L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) ∂μ
  _ = ∫ x, L x + ∫ y, L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) ∂μ := by
    congr with x
    rw [integral_add (by fun_prop) (by fun_prop)]
    simp [-ContinuousLinearEquiv.coe_neg, integral_const, smul_eq_mul]
  _ = ∫ x, L x ∂μ + ∫ y, L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) := by
    rw [integral_add (by fun_prop) (by fun_prop)]
    simp
  _ = 0 := by
    rw [integral_map (by fun_prop) (by fun_prop)]
    simp [integral_neg]

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

Goal state before:
pp: case hv.hX
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEStronglyMeasurable (fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis i, u⟫)
    (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))

pp: case hv.hY
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEStronglyMeasurable (fun u ↦ ⟪(EuclideanSpace.basisFun ↥J ℝ).toBasis j, u⟫)
    (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))

pp: case hv.hZ
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEMeasurable (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S)

pp: case hv.h
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ MemLp id 2 (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))

Tactic:
any_goals exact Measurable.aestronglyMeasurable (by fun_prop)

Goal state after:
case hv.hZ
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEMeasurable (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S)

case hv.h
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ MemLp id 2 (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))
Module: Mathlib.Probability.Process.FiniteDimensionalLaws

Goal state before:
pp: case refine_2
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h : IdentDistrib (fun ω x ↦ X x ω) (fun ω x ↦ Y x ω) P P
I : Finset T
⊢ AEMeasurable (fun ω ↦ I.restrict fun x ↦ Y x ω) P

pp: case refine_3
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h : IdentDistrib (fun ω x ↦ X x ω) (fun ω x ↦ Y x ω) P P
I : Finset T
⊢ Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P = Measure.map (fun ω ↦ I.restrict fun x ↦ Y x ω) P

pp: case refine_4
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h : ∀ (I : Finset T), IdentDistrib (fun ω ↦ I.restrict fun x ↦ X x ω) (fun ω ↦ I.restrict fun x ↦ Y x ω) P P
⊢ Measure.map (fun ω x ↦ X x ω) P = Measure.map (fun ω x ↦ Y x ω) P

Tactic:
· exact (Finset.measurable_restrict _).comp_aemeasurable hY

Goal state after:
case refine_3
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h : IdentDistrib (fun ω x ↦ X x ω) (fun ω x ↦ Y x ω) P P
I : Finset T
⊢ Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P = Measure.map (fun ω ↦ I.restrict fun x ↦ Y x ω) P

case refine_4
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h : ∀ (I : Finset T), IdentDistrib (fun ω ↦ I.restrict fun x ↦ X x ω) (fun ω ↦ I.restrict fun x ↦ Y x ω) P P
⊢ Measure.map (fun ω x ↦ X x ω) P = Measure.map (fun ω x ↦ Y x ω) P