mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: α : Type u
β : Type v
δ : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : (α : Type u) → [LinearOrder α] → (β : Type v) → [LinearOrder β] → δ
c :
  ∀ (α₁ : Type u) [inst : LinearOrder α₁] (β₁ : Type v) [inst_1 : LinearOrder β₁] (α₂ : Type u)
    [inst_2 : LinearOrder α₂] (β₂ : Type v) [inst_3 : LinearOrder β₂],
    type α₁ = type α₂ → type β₁ = type β₂ → f α₁ β₁ = f α₂ β₂
⊢ (type α).liftOn₂ (type β) f c = f α β

Tactic:
by rfl

Goal state after:
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
inst✝ : (i : ι) → MeasurableSpace (β i)
u : (i : ι) → Ω → β i
i : ι
hf : Adapted f u
⊢ inst✝ i ≤ inst✝ i

Tactic:
by rfl

Goal state after:
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
inst✝ : (i : ι) → MeasurableSpace (β i)
u : (i : ι) → Ω → β i
i j : ι
hf : Adapted f u
hij : i ≤ j
⊢ inst✝ i ≤ inst✝ i

Tactic:
by rfl

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

Goal state before:
pp: case refine_2
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this✝ : MeasurableSpace (ℕ × Ω) := ⋯
this : MeasurableSpace Ω := ⋯
X : ℕ → Ω → E := ⋯
m : ℕ
⊢ Set.range (X m) ⊆ Set.range ⇑(StronglyMeasurable.approx h𝓕 m)

Tactic:
Set.range_subset_iff

Goal state after:
case refine_2
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this✝ : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
this : MeasurableSpace Ω := ↑𝓕 n
X : ℕ → Ω → E := fun m ↦ Function.curry (⇑(StronglyMeasurable.approx h𝓕 m)) (n + 1)
m : ℕ
⊢ ∀ (y : Ω), X m y ∈ Set.range ⇑(StronglyMeasurable.approx h𝓕 m)
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✝ : SigmaFiniteFiltration μ ℱ
hf : IsStronglyPredictable ℱ f
hfint : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
⊢ martingalePart f ℱ μ n =ᵐ[μ] f 0

Tactic:
by
  filter_upwards [hf.predictablePart_eq (μ := μ) hfint n] with ω hω
  simp [martingalePart, hω, sub_eq_add_neg]

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

Goal state before:
pp: case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : IsMin i
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
suffices {ω : Ω | τ ω < i} = ∅ by rw [this]; exact @MeasurableSet.empty _ (f i)
    ext1 ω
    simp only [Set.mem_ofPred_eq, Set.mem_empty_iff_false, iff_false]
    rw [isMin_iff_forall_not_lt] at hi_min
    cases τ ω with
    | top => simp
    | coe t => exact mod_cast hi_min t

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
ω : Ω
⊢ (if ∃ j ∈ Set.Icc n m, u j ω ∈ Set.univ then sInf (Set.Icc n m) else m) = min n m

Tactic:
by_cases hnm : n ≤ m <;> simp [hnm]

Goal state after:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
ω : Ω
hnm : n ≤ m
⊢ (∀ (x : ι), n ≤ x → m < x) → m = n

case neg
Ω : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
ω : Ω
hnm : ¬n ≤ m
⊢ m ≤ n
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
⊢ hittingAfter u s n ω = ⊤ ↔ ∀ (j : ι), n ≤ j → u j ω ∉ s

Tactic:
by
  simp [hittingAfter]

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

Goal state before:
pp: case succ
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]
i j k : ℕ
hik : i ≤ k
hk : f i ≤ᵐ[μ] μ[f k | ↑𝒢 i]
⊢ f i ≤ᵐ[μ] μ[f (k + 1) | ↑𝒢 i]

Tactic:
filter_upwards [hk, condExp_mono (hint k) integrable_condExp (hf k),
      𝒢.condExp_condExp (f (k + 1)) hik] with ω hω1 hω2 hω3

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]
i j k : ℕ
hik : i ≤ k
hk : f i ≤ᵐ[μ] μ[f k | ↑𝒢 i]
ω : Ω
hω1 : f i ω ≤ μ[f k | ↑𝒢 i] ω
hω2 : μ[f k | ?m.143] ω ≤ μ[μ[f (k + 1) | ↑𝒢 k] | ?m.143] ω
hω3 : μ[μ[f (k + 1) | ↑𝒢 k] | ↑𝒢 i] ω = μ[f (k + 1) | ↑𝒢 i] ω
⊢ f i ω ≤ μ[f (k + 1) | ↑𝒢 i] ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos.coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : IsMin i
ω : Ω
t : ι
⊢ ¬t < i

Tactic:
exact isMin_iff_forall_not_lt.mp hi_min t

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

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
obtain ⟨seq, -, -, h_tendsto, h_bound⟩ :
      ∃ seq : ℕ → ι, Monotone seq ∧ (∀ j, seq j ≤ i) ∧ Tendsto seq atTop (𝓝 i) ∧ ∀ j, seq j < i :=
    h_lub.exists_seq_monotone_tendsto (not_isMin_iff.mp hi_min)

Goal state after:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
h_lub : IsLUB (Set.Iio i) i
hi_min : ¬IsMin i
seq : ℕ → ι
h_tendsto : Tendsto seq atTop (𝓝 i)
h_bound : ∀ (j : ℕ), seq j < i
⊢ MeasurableSet {ω | τ ω < ↑i}
Module: Mathlib.Probability.Martingale.Upcrossing

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

Tactic:
suffices Monotone fun n => lowerCrossingTime a b f N n ω by exact this hnm
  exact monotone_nat_of_le_succ fun n =>
    le_trans lowerCrossingTime_le_upperCrossingTime_succ upperCrossingTime_le_lowerCrossingTime

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
⊢ upperCrossingTime a b f N (n + 1) ω < lowerCrossingTime a b f N (n + 1) ω

Tactic:
refine lt_of_le_of_ne upperCrossingTime_le_lowerCrossingTime fun h =>
    not_le.2 hab <| le_trans ?_ (stoppedValue_lowerCrossingTime hn)

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω
⊢ b ≤ stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N (n + 1) ω)) ω
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: case succ
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i =ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]
i j k : ℕ
hik : i ≤ k
hk : μ[f k | ↑𝒢 i] =ᵐ[μ] f i
⊢ μ[f (k + 1) | ↑𝒢 i] =ᵐ[μ] f i

Tactic:
filter_upwards [hk, condExp_congr_ae (hf k), 𝒢.condExp_condExp (f (k + 1)) hik]
      with ω hω1 hω2 hω3

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i =ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]
i j k : ℕ
hik : i ≤ k
hk : μ[f k | ↑𝒢 i] =ᵐ[μ] f i
ω : Ω
hω1 : μ[f k | ↑𝒢 i] ω = f i ω
hω2 : μ[f k | ?m.127] ω = μ[μ[f (k + 1) | ↑𝒢 k] | ?m.127] ω
hω3 : μ[μ[f (k + 1) | ↑𝒢 k] | ↑𝒢 i] ω = μ[f (k + 1) | ↑𝒢 i] ω
⊢ μ[f (k + 1) | ↑𝒢 i] ω = f i ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : AddGroup ι
inst✝² : Preorder ι
inst✝¹ : AddRightMono ι
inst✝ : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
⊢ IsStoppingTime f fun ω ↦ τ ω + ↑i

Tactic:
intro j
  simp only
  have h_eq : {ω | τ ω + i ≤ j} = {ω | τ ω ≤ j - i} := by
    ext ω
    simp only [Set.mem_ofPred_eq, coe_sub]
    cases τ ω with
    | top => simp
    | coe a => norm_cast; simp_rw [← le_sub_iff_add_le]
  rw [h_eq]
  exact f.mono (sub_le_self j hi) _ (hτ (j - i))

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 β
inst✝ : (ω : Ω) → Decidable (∃ j, u j ω ∈ s)
ω : Ω
⊢ hittingAfter u s ⊥ ω = if ∃ j, u j ω ∈ s then ↑(sInf {i | u i ω ∈ s}) else ⊤

Tactic:
by
  simp [hittingAfter]

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst✝ : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ∞
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
hπ_bdd : ∃ N, ∀ (x : Ω), π x ≤ ↑N
⊢ ∫ (x : Ω), stoppedValue (stoppedProcess f τ) σ x ∂μ ≤ ∫ (x : Ω), stoppedValue (stoppedProcess f τ) π x ∂μ

Tactic:
simp_rw [stoppedValue_stoppedProcess]

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst✝ : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ∞
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
hπ_bdd : ∃ N, ∀ (x : Ω), π x ≤ ↑N
⊢ ∫ (x : Ω),
      if σ x ≠ ⊤ then stoppedValue f (fun ω ↦ min (σ ω) (τ ω)) x
      else stoppedValue f (fun ω ↦ min (↑(Classical.arbitrary ℕ)) (τ ω)) x ∂μ ≤
    ∫ (x : Ω),
      if π x ≠ ⊤ then stoppedValue f (fun ω ↦ min (π ω) (τ ω)) x
      else stoppedValue f (fun ω ↦ min (↑(Classical.arbitrary ℕ)) (τ ω)) x ∂μ
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case pos
Ω : 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
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
this : upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ : ¬∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N (k + 1) ω) N, (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
⊢ N = sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i | f i ω ≤ a})

Tactic:
refine False.elim (h₁ ?_)
      simp_all only [Set.mem_Iic]

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 ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
⊢ MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s

Tactic:
measurableSpace_min_const hτ

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
⊢ MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case mp
Ω : Type u_1
ι : Type u_3
inst✝¹ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
y : Ω
ω : ι
h : ω ∈ s ∧ τ y = ↑ω
⊢ ω = (τ y).untopA

Tactic:
simp [h.2]

Goal state after:
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
⊢ Integrable (fun ω ↦ rexp (t * X ω)) μ

Tactic:
refine Integrable.mono (ha.add hb) ?_ (ae_of_all _ fun ω ↦ ?_)

Goal state after:
case refine_1
Ω : 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
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) μ

case refine_2
Ω : 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 (t * X ω)‖ ≤ ‖((fun ω ↦ rexp (a * X ω)) + fun ω ↦ rexp (b * X ω)) ω‖
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 (stoppedProcess u τ n) p μ

Tactic:
rw [stoppedProcess_eq_of_mem_finset n hbdd]

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

Goal state before:
pp: case pos
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ ∂gaussianReal μ v/∂ℙ =ᵐ[ℙ] gaussianPDF μ v

pp: case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
⊢ ∂gaussianReal μ v/∂ℙ =ᵐ[ℙ] gaussianPDF μ v

Tactic:
· simp only [hv, gaussianReal_zero_var, gaussianPDF_zero_var]
    refine (Measure.eq_rnDeriv measurable_zero (mutuallySingular_dirac μ volume) ?_).symm
    rw [withDensity_zero, add_zero]

Goal state after:
case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
⊢ ∂gaussianReal μ v/∂ℙ =ᵐ[ℙ] gaussianPDF μ v
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 ∂μ
⊢ ((∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) / mgf X μ v ^ 2 = deriv (cgf X μ) v ^ 2

Tactic:
deriv_cgf h

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 =
    ((∫ (x : Ω), (fun ω ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v) ^ 2
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
⊢ deriv (cgf X μ) v ^ 2 =
    (2 * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v / mgf X μ v - deriv (cgf X μ) v ^ 2

pp: case e_a.hb
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ mgf X μ v ≠ 0

Tactic:
deriv_cgf h

Goal state after:
case e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ ((∫ (x : Ω), (fun ω ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v) ^ 2 =
    (2 * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * ((∫ (x : Ω), (fun ω ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v) /
        mgf X μ v -
      ((∫ (x : Ω), (fun ω ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v) ^ 2

case e_a.hb
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ mgf X μ v ≠ 0
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 * ↑v).toNNReal

Tactic:
Real.toNNReal_mul (by positivity),

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ Measure.map (⇑L) (gaussianReal μ v) = gaussianReal (L μ) ((L 1 ^ 2).toNNReal * v)

Tactic:
have : (L : ℝ → ℝ) = fun x ↦ L 1 * x := by simp
  rw [this, gaussianReal_map_const_mul]
  congr
  simp only [mul_one, left_eq_sup]
  positivity

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h_Lp : ¬MemLp id p μ
L : StrongDual 𝕜 E
⊢ (toLpₗ μ p) L = 0

Tactic:
simp [toLpₗ, dif_neg h_Lp]

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

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
⊢ ‖(toLpₗ μ p) L‖ ≤ ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
by_cases h_Lp : MemLp id p μ
  swap
  · simp only [h_Lp, not_false_eq_true, toLpₗ_of_not_memLp, Lp.norm_zero]
    positivity
  by_cases hp : p = 0
  · simp only [h_Lp, toLpₗ_apply, Lp.norm_toLp]
    simp [hp]
  by_cases hp_top : p = ∞
  · simp only [hp_top, StrongDual.toLpₗ_apply h_Lp, Lp.norm_toLp, eLpNorm_exponent_top] at h_Lp ⊢
    simp only [eLpNormEssSup, id_eq]
    suffices (essSup (fun x ↦ ‖L x‖ₑ) μ).toReal ≤ (essSup (fun x ↦ ‖L‖ₑ * ‖x‖ₑ) μ).toReal by
      rwa [ENNReal.essSup_const_mul, ENNReal.toReal_mul, toReal_enorm] at this
    gcongr
    · rw [ENNReal.essSup_const_mul]
      exact ENNReal.mul_ne_top (by simp) h_Lp.eLpNorm_ne_top
    · exact essSup_mono_ae <| ae_of_all _ L.le_opENorm
  have h0 : 0 < p.toReal := by simp [ENNReal.toReal_pos_iff, pos_iff_ne_zero, hp, Ne.lt_top hp_top]
  suffices ‖L.toLpₗ μ p‖
      ≤ (‖L‖ₑ ^ p.toReal * ∫⁻ x, ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹ by
    refine this.trans_eq ?_
    simp only [ENNReal.toReal_mul]
    rw [← ENNReal.toReal_rpow, Real.mul_rpow (by positivity) (by positivity),
      ← Real.rpow_mul (by positivity), mul_inv_cancel₀ h0.ne', Real.rpow_one, toReal_enorm]
    rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by simp [hp]) hp_top, ENNReal.toReal_rpow]
    simp
  rw [StrongDual.toLpₗ_apply h_Lp, Lp.norm_toLp,
    eLpNorm_eq_lintegral_rpow_enorm_toReal (by simp [hp]) hp_top]
  simp only [one_div]
  refine ENNReal.toReal_le_of_le_ofReal (by positivity) ?_
  suffices ∫⁻ x, ‖L x‖ₑ ^ p.toReal ∂μ ≤ ‖L‖ₑ ^ p.toReal * ∫⁻ x, ‖x‖ₑ ^ p.toReal ∂μ by
    rw [← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity)]
    gcongr
    rwa [ENNReal.ofReal_toReal]
    refine ENNReal.mul_ne_top (by simp) ?_
    have h := h_Lp.eLpNorm_ne_top
    rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by simp [hp]) hp_top] at h
    simpa [h0] using h
  calc ∫⁻ x, ‖L x‖ₑ ^ p.toReal ∂μ
  _ ≤ ∫⁻ x, ‖L‖ₑ ^ p.toReal * ‖x‖ₑ ^ p.toReal ∂μ := by
    refine lintegral_mono fun x ↦ ?_
    rw [← ENNReal.mul_rpow_of_nonneg]
    swap; · positivity
    gcongr
    exact L.le_opENorm x
  _ = ‖L‖ₑ ^ p.toReal * ∫⁻ x, ‖x‖ₑ ^ p.toReal ∂μ := by rw [lintegral_const_mul]; fun_prop

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✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
C C' : ℝ
hint : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
y : E
hy : Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
this : ∀ (x : E), rexp (C' * ‖x‖ ^ 2) ≤ rexp (C / ε * ‖y‖ ^ 2) * rexp (C * ‖x - y‖ ^ 2)
⊢ Integrable (fun x ↦ rexp (C' * ‖x‖ ^ 2)) μ

Tactic:
refine integrable_of_le_of_le (g₁ := 0)
      (g₂ := fun x ↦ rexp (C / ε * ‖y‖ ^ 2) * rexp (C * ‖x - y‖ ^ 2)) (by fun_prop) ?_ ?_
      (integrable_const _) (hy.const_mul _)
    · exact ae_of_all _ fun _ ↦ by positivity
    · exact ae_of_all _ this

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a✝ : α
q : ℚ
a : β
ha : IsRatStieltjesPoint f (a✝, a)
⊢ toRatCDF f (a✝, a) q = f (a✝, a) q

Tactic:
toRatCDF_of_isRatStieltjesPoint ha

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a✝ : α
q : ℚ
a : β
ha : IsRatStieltjesPoint f (a✝, a)
⊢ f (a✝, a) q = f (a✝, a) q
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ ContinuousWithinAt (stieltjesFunctionAux f a) (Ici x) x

Tactic:
rw [← continuousWithinAt_Ioi_iff_Ici]
  convert! Monotone.tendsto_nhdsGT (monotone_stieltjesFunctionAux hf a) x
  rw [sInf_image']
  have h' : ⨅ r : Ioi x, stieltjesFunctionAux f a r
      = ⨅ r : { r' : ℚ // x < r' }, stieltjesFunctionAux f a r := by
    refine Real.iInf_Ioi_eq_iInf_rat_gt x ?_ (monotone_stieltjesFunctionAux hf a)
    refine ⟨0, fun z ↦ ?_⟩
    rintro ⟨u, -, rfl⟩
    exact stieltjesFunctionAux_nonneg hf a u
  have h'' :
    ⨅ r : { r' : ℚ // x < r' }, stieltjesFunctionAux f a r =
      ⨅ r : { r' : ℚ // x < r' }, f a r := by
    congr with r
    exact stieltjesFunctionAux_eq hf a r
  rw [h', h'', ContinuousWithinAt]
  congr!
  rw [stieltjesFunctionAux_def]

Goal state after: