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:
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: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
E : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
u : ι → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
i : ι
this✝ : MeasurableSpace (ι × Ω) := 𝓕.predictable
this : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑𝓕 i)
⊢ StronglyMeasurable fun p ↦ u (↑p.1) p.2

Tactic:
let X m (x : Set.Iic i × Ω) := h𝓕.approx m ⟨x.1, x.2⟩

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
E : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
u : ι → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
i : ι
this✝ : MeasurableSpace (ι × Ω) := 𝓕.predictable
this : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑𝓕 i)
X : ℕ → ↑(Set.Iic i) × Ω → E := fun m_1 x ↦ (StronglyMeasurable.approx h𝓕 m_1) (↑x.1, x.2)
⊢ StronglyMeasurable fun p ↦ u (↑p.1) p.2
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
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
h_lt :
  ∀ k < i,
    μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] f (k + 1) - f k - μ[f (k + 1) - f k | ↑ℱ k]
⊢ ∑ k ∈ Finset.range i, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i]) +
      ∑ k ∈ Finset.Ico i j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i]) =ᵐ[μ]
    ∑ i ∈ Finset.range i, (f (i + 1) - f i - μ[f (i + 1) - f i | ↑ℱ i]) + 0

Tactic:
refine (eventuallyEq_sum fun k hk => h_lt k (Finset.mem_range.mp hk)).add ?_

Goal state after:
Ω : 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
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
h_lt :
  ∀ k < i,
    μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] f (k + 1) - f k - μ[f (k + 1) - f k | ↑ℱ k]
⊢ ∑ k ∈ Finset.Ico i j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i]) =ᵐ[μ] 0
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 β
n m : ι
ω : Ω
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ m ≤ m

Tactic:
· exact le_rfl

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

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω = ↑i} = {ω | τ ω ≤ ↑i} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < ↑i), {ω | τ ω ≤ j}
j : WithTop ι
x✝ : j ∈ Set.range τ
hji : ¬j < ↑i
⊢ MeasurableSet ∅

Tactic:
· exact @MeasurableSet.empty _ (f i)

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
⊢ BddAbove {n | upperCrossingTime a b f N n ω < N}

Tactic:
by
  obtain ⟨k, hk⟩ := exists_upperCrossingTime_eq f N ω hab
  refine ⟨k, fun n (hn : upperCrossingTime a b f N n ω < N) => ?_⟩
  by_contra hn'
  exact hn.ne (upperCrossingTime_stabilize (not_le.1 hn').le hk)

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m i : ι
hi : i < m
⊢ hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s

Tactic:
by_cases h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
  · rw [hittingBtwn_le_iff_of_exists h_exists]
  · simp_rw [hittingBtwn, if_neg h_exists]
    push Not at h_exists
    simp only [not_le.mpr hi, Set.mem_Icc, false_iff, not_exists, not_and, and_imp]
    exact fun k hkn hki => h_exists k ⟨hkn, hki.trans hi.le⟩

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

Goal state before:
pp: case zero.hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : hittingBtwn f (Set.Iic a) (upperCrossingTime a b f N 0 ω) N ω < N
h' : upperCrossingTime a b f N 0 ω < N
⊢ N ≤ N

Tactic:
· exact le_rfl

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

Goal state before:
pp: Ω : 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 : lowerCrossingTime a b f N (k + 1) ω < N
j : ℕ
hj₁ : j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N
hj₂ : f j ω ∈ Set.Ici b
⊢ hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f M k ω) M ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω

Tactic:
rw [eq_comm, ih.2]

Goal state after:
Ω : 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 : lowerCrossingTime a b f N (k + 1) ω < N
j : ℕ
hj₁ : j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N
hj₂ : f j ω ∈ Set.Ici b
⊢ hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) M ω
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case hi
Ω : 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 : lowerCrossingTime a b f N (k + 1) ω < N
h' : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω < N
⊢ N ≤ N

Tactic:
· exact le_rfl

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

Goal state before:
pp: case hi
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ N ≤ N

Tactic:
· exact le_rfl

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b, a_1 ≤ b ∧ f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1, a ≤ b_1 ∧ b < f b_1 ω
⊢ False

Tactic:
refine Classical.not_not.2 hω ?_

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b, a_1 ≤ b ∧ f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1, a ≤ b_1 ∧ b < f b_1 ω
⊢ ¬∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
Module: Mathlib.Probability.Martingale.Upcrossing

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

Tactic:
simp only [lowerCrossingTime, this, hittingBtwn, Set.mem_Iic]

Goal state after:
case succ
Ω : 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)
ω : Ω
⊢ (if ∃ j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N (k + 1) ω) N, (f j ω - a)⁺ ∈ Set.Iic 0 then
      sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i | (f i ω - a)⁺ ≤ 0})
    else N) =
    if ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a then
      sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i | f i ω ≤ a})
    else N
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : b - a ≤ 0
⊢ 0 * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ

Tactic:
zero_mul

Goal state after:
case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : b - a ≤ 0
⊢ 0 ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
hμ : μ ≠ 0
h_int_X : Integrable (fun ω ↦ rexp (t * X ω)) μ
this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ
⊢ 0 < μ ((Function.support fun x ↦ rexp (t * X x)) ∩ Set.univ)

Tactic:
have h_eq_univ : (Function.support fun x : Ω => exp (t * X x)) = Set.univ := by
      ext1 x
      simp only [Function.mem_support, Set.mem_univ, iff_true]
      exact (exp_pos _).ne'
    rw [h_eq_univ, Set.inter_univ _]
    refine Ne.bot_lt ?_
    simp only [hμ, ENNReal.bot_eq_zero, Ne, Measure.measure_univ_eq_zero, not_false_iff]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ mgf (fun ω ↦ X ω + α) μ t = mgf X μ t * rexp (t * α)

Tactic:
by
  simp only [add_comm, mgf_const_add, mul_comm]

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

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

Tactic:
lift τ y to ι using this with i hi

Goal state after:
case mpr
Ω : Type u_1
ι : Type u_3
inst✝¹ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
y : Ω
ω i : ι
hi : ↑i = τ y
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ω = (↑i).untopA
⊢ (↑i).untopA ∈ s ∧ ↑i = ↑(↑i).untopA
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 ≤ τ ω
⊢ stoppedProcess u τ n ω = {a | ↑n ≤ τ a}.indicator (u n) ω + ∑ c ∈ s with c < n, {ω | τ ω = ↑c}.indicator (u c) ω

Tactic:
rw [stoppedProcess_eq_of_le h, Set.indicator_of_mem, Finset.sum_eq_zero, add_zero]
    · intro m hm
      refine Set.indicator_of_notMem ?_ _
      rw [Finset.mem_filter] at hm
      simp only [Set.mem_ofPred_eq]
      refine (lt_of_lt_of_le ?_ h).ne'
      exact mod_cast hm.2
    · exact h

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

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

Tactic:
rcases lt_or_gt_of_ne ht with ht_neg | ht_pos

Goal state after:
case inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))

case inr
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_pos : 0 < t
⊢ |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
hz : z.re ∈ integrableExpSet X μ
⊢ Integrable (fun ω ↦ cexp (z * ↑(X ω))) μ

Tactic:
rw [← integrable_norm_iff]
  · simpa [Complex.norm_exp] using! hz
  · fun_prop

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

Goal state before:
pp: case hb
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
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
⊢ essSup (fun x ↦ ‖L‖ₑ * ‖x‖ₑ) μ ≠ ∞

Tactic:
rw [ENNReal.essSup_const_mul]

Goal state after:
case hb
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
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
⊢ ‖L‖ₑ * essSup enorm μ ≠ ∞
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (fun x ↦ x - c) p μ
this : id = fun x ↦ x - c + c
hx : ¬c = 0
hp0 : p ≠ 0
hptop : p ≠ ∞
⊢ Integrable (fun x ↦ ‖x‖) μ

Tactic:
apply Integrable.norm

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ⋯
h_Lp : MemLp (fun x ↦ x - c) p μ
this : id = fun x ↦ x - c + c
hx : ¬c = 0
hp0 : p ≠ 0
hptop : p ≠ ∞
⊢ Integrable (fun a ↦ a) μ
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
⊢ logRatio c * normThreshold a (n + 1) ^ 2 * a⁻¹ ^ 2 ≤ 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n

Tactic:
by
  by_cases ha : a = 0
  · simp only [ha, inv_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, mul_zero,
      Nat.ofNat_pos, pow_pos, mul_nonneg_iff_of_pos_right, inv_pos, mul_nonneg_iff_of_pos_left]
    refine Real.log_nonneg ?_
    rw [one_le_div]
    · refine (ENNReal.toReal_le_toReal (by finiteness) (by finiteness)).mpr ?_
      refine tsub_le_iff_left.mpr ?_
      rw [← two_mul]
      rw [inv_eq_one_div, ENNReal.div_lt_iff (by simp) (by simp), mul_comm] at hc_gt
      exact hc_gt.le
    · simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hc_lt, true_and]
      finiteness
  calc logRatio c * normThreshold a (n + 1) ^ 2 * a⁻¹ ^ 2
  _ ≤ logRatio c * (a ^ 2 * (1 + √2) ^ 2 * 2 ^ (n + 2)) * a⁻¹ ^ 2 := by
    gcongr
    · exact (logRatio_pos hc_gt hc_lt).le
    · exact sq_normThreshold_add_one_le n
  _ = 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n := by
    unfold logRatio
    field

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : Ω → E
inst✝ : InnerProductSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
t : E
⊢ charFun (Measure.map (X + Y) P) t = (charFun (Measure.map X P) * charFun (Measure.map Y P)) t

Tactic:
hXY.map_add_eq_map_conv_map₀ mX mY,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : Ω → E
inst✝ : InnerProductSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
t : E
⊢ charFun (Measure.map X P ∗ Measure.map Y P) t = (charFun (Measure.map X P) * charFun (Measure.map Y P)) t
Module: Mathlib.Probability.Process.FiniteDimensionalLaws

Goal state before:
pp: T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X : (t : T) → Ω → 𝓧 t
P : Measure Ω
hX : ∀ (t : T), AEMeasurable (X t) P
I J : Finset T
hJI : J ⊆ I
⊢ (fun I ↦ Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P) J =
    Measure.map (Finset.restrict₂ hJI) ((fun I ↦ Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P) I)

Tactic:
rw [AEMeasurable.map_map_of_aemeasurable (Finset.measurable_restrict₂ _).aemeasurable]

Goal state after:
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X : (t : T) → Ω → 𝓧 t
P : Measure Ω
hX : ∀ (t : T), AEMeasurable (X t) P
I J : Finset T
hJI : J ⊆ I
⊢ (fun I ↦ Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P) J =
    Measure.map (Finset.restrict₂ hJI ∘ fun ω ↦ I.restrict fun x ↦ X x ω) P

T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X : (t : T) → Ω → 𝓧 t
P : Measure Ω
hX : ∀ (t : T), AEMeasurable (X t) P
I J : Finset T
hJI : J ⊆ I
⊢ AEMeasurable (fun ω ↦ I.restrict fun x ↦ X x ω) P
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : Ω → E
inst✝ : NormedSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
L : StrongDual ℝ E
⊢ charFunDual (Measure.map (X + Y) P) L = (charFunDual (Measure.map X P) * charFunDual (Measure.map Y P)) L

Tactic:
hXY.map_add_eq_map_conv_map₀ mX mY,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : Ω → E
inst✝ : NormedSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
L : StrongDual ℝ E
⊢ charFunDual (Measure.map X P ∗ Measure.map Y P) L = (charFunDual (Measure.map X P) * charFunDual (Measure.map Y P)) L
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
c : ℝ≥0∞
hc : c ≤ μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha : 0 ≤ a
ha_pos : 0 < a
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c)) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * 2 ^ n))

Tactic:
| inr ha_pos =>

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 : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (x_1 : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, x_1)) x) ∂ν a = (κ a) (s ×ˢ Iic x)

pp: case hfi
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ((ν a).restrict s)

pp: case f_nn
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ 0 ≤ᵐ[(ν a).restrict s] fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x

Tactic:
setLIntegral_stieltjesOfMeasurableRat hf _ _ hs

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ (κ a) (s ×ˢ Iic x) = (κ a) (s ×ˢ Iic x)

case hfi
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ((ν a).restrict s)

case f_nn
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ 0 ≤ᵐ[(ν a).restrict s] fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case refine_4
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
⊢ ∀ᵐ (a_1 : β) ∂ν a, ∀ (i : ℕ), f (a, a_1) (seq i) ≤ 1

Tactic:
· filter_upwards [hf.le_one a] with c hc using fun i ↦ hc (seq i)

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Antitone s
hs_tendsto : Tendsto s atTop atBot
⊢ Tendsto (fun m ↦ ∫ (c : α), (preCDF ρ (s m) (a, c).2).toReal ∂(Kernel.const Unit ρ.fst) a) atTop (𝓝 0)

Tactic:
simp_rw [Kernel.const_apply, integral_preCDF_fst ρ]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Antitone s
hs_tendsto : Tendsto s atTop atBot
⊢ Tendsto (fun m ↦ (ρ.IicSnd ↑(s m)).real univ) atTop (𝓝 0)
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto (fun m ↦ ∫ (c : α), (preCDF ρ (s m) (a, c).2).toReal ∂(Kernel.const Unit ρ.fst) a) atTop
    (𝓝 (((Kernel.const Unit ρ.fst) a).real univ))

Tactic:
simp_rw [Kernel.const_apply, integral_preCDF_fst ρ]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto (fun m ↦ (ρ.IicSnd ↑(s m)).real univ) atTop (𝓝 (ρ.fst.real univ))