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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
β : Type u_3
u : ι → Ω → β
mi : MeasurableSpace ι
mβ : MeasurableSpace β
t : ι → Ω → ι
h : IsProgressive f u
ht : IsProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
⊢ IsProgressive f fun i ω ↦ u (t i ω) ω

Tactic:
by
  intro i
  have : (fun p : ↥(Set.Iic i) × Ω => u (t (p.fst : ι) p.snd) p.snd) =
    (fun p : ↥(Set.Iic i) × Ω => u (p.fst : ι) p.snd) ∘ fun p : ↥(Set.Iic i) × Ω =>
      (⟨t (p.fst : ι) p.snd, Set.mem_Iic.mpr ((ht_le _ _).trans p.fst.prop)⟩, p.snd) := rfl
  rw [this]
  exact (h i).comp ((ht i).subtype_mk.prodMk measurable_snd)

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

Goal state before:
pp: case inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : j ≤ i
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)

pp: case inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : i ≤ j
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)

Tactic:
· simp [hij]

Goal state after:
case inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : i ≤ j
⊢ MeasurableSet (Set.Ioc i j ×ˢ s)
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
⊢ hittingBtwn u s m m ω = m

Tactic:
rw [hittingBtwn, ite_eq_right_iff, forall_exists_index]
    conv => intro; rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]
    intro i hi₁ hi₂ hi
    rw [Set.inter_eq_left.2, csInf_singleton]
    exact Set.singleton_subset_iff.2 (le_antisymm hi₂ hi₁ ▸ hi)

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find ⋯
m : ℕ
hm : m < (Nat.find ⋯).pred
⊢ upperCrossingTime a b f N (m + 1) ω ≠ N

Tactic:
Nat.lt_pred_iff

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find ⋯
m : ℕ
hm : m.succ < Nat.find ⋯
⊢ upperCrossingTime a b f N (m + 1) ω ≠ N
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hE : ¬∃ j ∈ Set.Icc n m, u j ω ∈ E
t : ι
ht : t ∈ Set.Icc n m ∧ u t ω ∈ F
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ F}) ≤ m

Tactic:
exact csInf_le_of_le ⟨n, by simp [mem_lowerBounds]; grind⟩ ht ht.1.2

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

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
m n n' : ι
hnn' : n ≤ n'
ω : Ω
h_n' : ¬∃ j ∈ Set.Icc n' m, u j ω ∈ s
t : ι
ht : t ∈ Set.Icc n m ∧ u t ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ m

Tactic:
exact csInf_le_of_le ⟨n, by simp [mem_lowerBounds]; grind⟩ ht ht.1.2

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_notMem_s : ∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)
⊢ ⊤ = sInf {i | u i ω ∈ s}

Tactic:
symm

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CompleteLattice ι
u : ι → Ω → β
s : Set β
ω : Ω
h_notMem_s : ∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)
⊢ sInf {i | u i ω ∈ s} = ⊤
Module: Mathlib.Probability.Process.Stopping

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

Tactic:
· simp [hij]

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

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

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 StronglyAdapted.stoppedProcess_of_discrete h.stronglyAdapted hτ

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

Goal state before:
pp: case refine_2
Ω : 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))) ω
ω : Ω
hω : ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
B : ℝ
hB : B ∈ upperBounds (Set.range fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)))
n : ℕ
⊢ ¬↑B.toNNReal < ∑ k ∈ Finset.range n, μ (s (k + 1))

Tactic:
mem_upperBounds

Goal state after:
case refine_2
Ω : 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))) ω
ω : Ω
hω : ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
B : ℝ
hB : ∀ x ∈ Set.range fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)), x ≤ B
n : ℕ
⊢ ¬↑B.toNNReal < ∑ k ∈ Finset.range n, μ (s (k + 1))
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᵐ[μ] Y
ht : t ≤ 0
htX : Integrable (fun ω ↦ rexp (t * X ω)) μ
htY : ¬Integrable (fun ω ↦ rexp (t * Y ω)) μ
⊢ mgf Y μ t ≤ mgf X μ t

Tactic:
mgf_undef htY

Goal state after:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᵐ[μ] Y
ht : t ≤ 0
htX : Integrable (fun ω ↦ rexp (t * X ω)) μ
htY : ¬Integrable (fun ω ↦ rexp (t * Y ω)) μ
⊢ 0 ≤ mgf X μ t
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 ≤ τ ω
⊢ ∀ x ∈ {i ∈ s | i < n}, {ω | τ ω = ↑x}.indicator (u x) ω = 0

Tactic:
intro m 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.Martingale.BorelCantelli

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

Tactic:
mem_upperBounds

Goal state after:
case mp
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
ω✝ : Ω
hω₁ : BddAbove (Set.range fun n ↦ f n ω✝) ↔ ∃ c, Tendsto (fun n ↦ f n ω✝) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n ↦ (-f) n ω✝) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω✝) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n ↦ f n ω✝) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω✝) atTop (𝓝 c)
c : ℝ
hc : ∀ x ∈ Set.range fun n ↦ (-f) n ω✝, x ≤ c
ω : ℝ
hω : ω ∈ Set.range fun n ↦ f n ω✝
⊢ -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
⊢ ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ f n ω) atTop atTop

Tactic:
by
  filter_upwards [hf.bddAbove_range_iff_bddBelow_range hbdd] with ω hω htop using
    not_bddAbove_of_tendsto_atTop htop (hω.2 <| bddBelow_range_of_tendsto_atTop_atTop htop)

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
⊢ MemLp ({a | ↑n ≤ τ a}.indicator (u n) + ∑ i ∈ s with i < n, {ω | τ ω = ↑i}.indicator (u i)) p μ

Tactic:
refine MemLp.add ?_ ?_

Goal state after:
case refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
⊢ MemLp ({a | ↑n ≤ τ a}.indicator (u n)) p μ

case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
⊢ MemLp (∑ i ∈ s with i < n, {ω | τ ω = ↑i}.indicator (u i)) p μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2
Ω : 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 (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)

Tactic:
rcases le_total 0 (X ω) with h_nonneg | h_nonpos

Goal state after:
case refine_2.inl
Ω : 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)) μ
ω : Ω
h_nonneg : 0 ≤ X ω
⊢ rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)

case refine_2.inr
Ω : 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)) μ
ω : Ω
h_nonpos : X ω ≤ 0
⊢ rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
⊢ ∀ (ω : Ω), ↑(π ω) ≠ ∞

pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
⊢ (fun ω ↦ (∑ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (i + 1) - u i)) ω) = fun ω ↦
    (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ ↑i ∧ ↑i < π ω}.indicator (u (i + 1) - u i)) ω

Tactic:
· intro ω; exact mod_cast hπ_top ω

Goal state after:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ ↑N
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
⊢ (fun ω ↦ (∑ i ∈ Finset.Ico (untopA (τ ω)) (untopA (π ω)), (u (i + 1) - u i)) ω) = fun ω ↦
    (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ ↑i ∧ ↑i < π ω}.indicator (u (i + 1) - u i)) ω
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✝³ : OpensMeasurableSpace E
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
h : Integrable id μ
L : E →L[𝕜] F
⊢ ∫ (x : F), x ∂Measure.map (⇑L) μ = L (∫ (x : E), x ∂μ)

Tactic:
integral_map (by fun_prop) (by fun_prop)

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✝³ : OpensMeasurableSpace E
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
h : Integrable id μ
L : E →L[𝕜] F
⊢ ∫ (x : E), L x ∂μ = L (∫ (x : E), x ∂μ)
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
this : g = fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-↑(2 * v)⁻¹ * x ^ 2)
⊢ Integrable g ℙ

Tactic:
rw [this]
      refine (integrable_exp_neg_mul_sq ?_).const_mul (√(2 * π * v))⁻¹
      simpa [pos_iff_ne_zero]

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

Goal state before:
pp: case e'_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ Set.univ = interior (integrableExpSet X μ)

Tactic:
symm

Goal state after:
case e'_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ interior (integrableExpSet X μ) = Set.univ
Module: Mathlib.Probability.Moments.IntegrableExpMul

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

Tactic:
rw [abs_of_nonpos hx]
      simp only [neg_mul, mul_neg, sup_eq_right, exp_le_exp, le_neg_self_iff]
      exact mul_nonpos_of_nonneg_of_nonpos (abs_nonneg _) hx

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

Goal state before:
pp: 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|

Tactic:
symm

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.IntegrableExpMul

Goal state before:
pp: l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v + min (v - l) (u - v) ≤ v + (u - v)

Tactic:
gcongr; exact inf_le_right

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

Goal state before:
pp: case neg
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ (Measure.map (⇑e.symm) (gaussianReal μ v)) s' = (gaussianReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)) s'

Tactic:
rw [MeasurableEquiv.gaussianReal_map_symm_apply hv e he' hs',
    gaussianReal_apply_eq_integral _ _ s']

Goal state after:
case neg
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal (∫ (x : ℝ) in s', |c⁻¹| * gaussianPDFReal μ v (e x)) =
    ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v) x)

μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ NNReal.mk (c ^ 2) ⋯ * v ≠ 0
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ ∫ (ω : ℝ), (ω - μ) ^ 2 ∂gaussianReal μ v = ∫ (ω : ℝ), ω ^ 2 ∂Measure.map (fun x ↦ x - μ) (gaussianReal μ v)

Tactic:
integral_map (by fun_prop) (by fun_prop)

Goal state after:
μ : ℝ
v : ℝ≥0
⊢ ∫ (ω : ℝ), (ω - μ) ^ 2 ∂gaussianReal μ v = ∫ (x : ℝ), (x - μ) ^ 2 ∂gaussianReal μ v
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 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
⊢ ∫ (z : E),
      ⟪x, z - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫ *
        ⟪y, z - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫ ∂Measure.map (fun x ↦ c + x) μ =
    ∫ (z : E), ⟪x, z - ∫ (x : E), id x ∂μ⟫ * ⟪y, z - ∫ (x : E), id x ∂μ⟫ ∂μ

Tactic:
integral_map (by fun_prop) (by fun_prop)

Goal state after:
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 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
⊢ ∫ (x_1 : E),
      ⟪x, c + x_1 - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫ *
        ⟪y, c + x_1 - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫ ∂μ =
    ∫ (z : E), ⟪x, z - ∫ (x : E), id x ∂μ⟫ * ⟪y, z - ∫ (x : E), id x ∂μ⟫ ∂μ
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 : ℝ
⊢ (Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ)) {p | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} =
    (μ.prod μ) {p | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2}

Tactic:
Measure.map_apply (by fun_prop)

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 : ℝ
⊢ (μ.prod μ) (⇑(ContinuousLinearMap.rotation (-(π / 4))) ⁻¹' {p | ‖p.1‖ ≤ a ∧ b < ‖p.2‖}) =
    (μ.prod μ) {p | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2}

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 : ℝ
⊢ MeasurableSet {p | ‖p.1‖ ≤ a ∧ b < ‖p.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 : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
⊢ (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 ≤ min ‖p.1‖ ‖p.2‖

Tactic:
by
      have := norm_add_sub_norm_sub_le_two_mul_min p.1 p.2
      linarith

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

Goal state before:
pp: case h₂
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
x : E
⊢ ‖L₂ x‖ ≤ ‖L₂‖ * ‖x‖

Tactic:
exact ContinuousLinearMap.le_opNorm L₂ x

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
μ : Measure E
inst✝¹ : IsGaussian μ
inst✝ : SecondCountableTopology E
L : StrongDual ℝ E
⊢ ∫ (x : E), L x ∂μ + ∫ (y : E), L y ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ = 0

Tactic:
integral_map (by fun_prop) (by fun_prop)

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : IsGaussian μ
inst✝ : SecondCountableTopology E
L : StrongDual ℝ E
⊢ ∫ (x : E), L x ∂μ + ∫ (x : E), L ((ContinuousLinearEquiv.neg ℝ) x) ∂μ = 0