mathlib-initiative/mathlib-tactics huggingface dataset:
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 μ ℱ
⊢ Martingale (martingalePart f ℱ μ) ℱ μ

Tactic:
refine ⟨stronglyAdapted_martingalePart hf, fun i j hij => ?_⟩
  -- ⊢ μ[martingalePart f ℱ μ j | ℱ i] =ᵐ[μ] martingalePart f ℱ μ i
  have 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]) := by
    rw [martingalePart_eq_sum]
    refine (condExp_add (hf_int 0) (by fun_prop) _).trans ?_
    refine (EventuallyEq.rfl.add (condExp_finsetSum (fun i _ => by fun_prop) _)).trans ?_
    refine EventuallyEq.add ?_ ?_
    · rw [condExp_of_stronglyMeasurable (ℱ.le _) _ (hf_int 0)]
      · exact (hf 0).mono (ℱ.mono zero_le)
    · exact eventuallyEq_sum fun k _ => condExp_sub (by fun_prop) integrable_condExp _
  refine h_eq_sum.trans ?_
  have h_ge : ∀ k, i ≤ k →
      μ[f (k + 1) - f k | ℱ i] - μ[μ[f (k + 1) - f k | ℱ k] | ℱ i] =ᵐ[μ] 0 := by
    intro k hk
    have : μ[μ[f (k + 1) - f k | ℱ k] | ℱ i] =ᵐ[μ] μ[f (k + 1) - f k | ℱ i] :=
      condExp_condExp_of_le (ℱ.mono hk) (ℱ.le k)
    filter_upwards [this] with x hx
    rw [Pi.sub_apply, Pi.zero_apply, hx, sub_self]
  have h_lt : ∀ k, 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] := by
    refine fun k hk => EventuallyEq.sub ?_ ?_
    · rw [condExp_of_stronglyMeasurable]
      · exact ((hf (k + 1)).mono (ℱ.mono (Nat.succ_le_of_lt hk))).sub ((hf k).mono (ℱ.mono hk.le))
      · exact (hf_int _).sub (hf_int _)
    · rw [condExp_of_stronglyMeasurable]
      · exact stronglyMeasurable_condExp.mono (ℱ.mono hk.le)
      · exact integrable_condExp
  rw [martingalePart_eq_sum]
  refine EventuallyEq.add EventuallyEq.rfl ?_
  rw [← Finset.sum_range_add_sum_Ico _ hij, ←
    add_zero (∑ i ∈ Finset.range i, (f (i + 1) - f i - μ[f (i + 1) - f i | ℱ i]))]
  refine (eventuallyEq_sum fun k hk => h_lt k (Finset.mem_range.mp hk)).add ?_
  refine (eventuallyEq_sum fun k hk => h_ge k (Finset.mem_Ico.mp hk).1).trans ?_
  simp only [Finset.sum_const_zero]
  rfl

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

Goal state before:
pp: case refine_1.top
Ω : 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 : ∀ s ∈ 𝓝 i, ∃ a, ∀ (b : ℕ), a ≤ b → seq b ∈ s
h_bound : ∀ (j : ℕ), seq j < i
hk_lt_i : ⊤ < ↑i
⊢ ∃ i, ⊤ ≤ ↑(seq i)

Tactic:
simp at hk_lt_i

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

Goal state before:
pp: Ω : 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]
⊢ Martingale f 𝒢 μ

Tactic:
by
  refine ⟨hadp, fun i j hij ↦ ?_⟩
  induction j, hij using Nat.le_induction with
  | base =>
    refine ae_of_all _ fun _ ↦ ?_
    rw [condExp_of_stronglyMeasurable (𝒢.le i) (hadp i) (hint i)]
  | succ k hik hk =>
    filter_upwards [hk, condExp_congr_ae (hf k), 𝒢.condExp_condExp (f (k + 1)) hik]
      with ω hω1 hω2 hω3
    rw [← hω1, hω2, hω3]

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

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

Tactic:
refine False.elim (h₂ ?_)

Goal state after:
case neg
Ω : 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
ω : Ω
h₁ : ∃ j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω ↦ (f n ω - a)⁺) N k ω) N, (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ¬∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
⊢ ∃ j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N, f j ω ∈ Set.Ici b
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω ↦ if h : ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c) then h.choose else 0
hle : ⨆ n, ↑ℱ n ≤ m0
⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω))

Tactic:
have hg' : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω)) := by
    filter_upwards [hf.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω
    simp_rw [g', dif_pos hω]
    exact hω.choose_spec

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω ↦ if h : ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c) then h.choose else 0
hle : ⨆ n, ↑ℱ n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g' ω))
⊢ ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω))
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✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet {ω | τ ω = ↑i}

Tactic:
← Set.univ_inter {ω | τ ω = i},

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet (Set.univ ∩ {ω | τ ω = ↑i})
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case neg
Ω : 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
⊢ sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i | (f i ω - a)⁺ ≤ 0}) = N

Tactic:
refine False.elim (h₂ ?_)

Goal state after:
case neg
Ω : 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
⊢ ∃ j ∈ Set.Icc (upperCrossingTime a b f N (k + 1) ω) N, f j ω ∈ Set.Iic a
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✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | ↑i ≤ τ ω} ↔ ω ∈ {ω | τ ω = ↑i} ∪ {ω | ↑i < τ ω}

Tactic:
simp only [le_iff_lt_or_eq, Set.mem_ofPred_eq, Set.mem_union]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ↑i < τ ω ∨ ↑i = τ ω ↔ τ ω = ↑i ∨ ↑i < τ ω
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 τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet {ω | τ ω = ↑i}

Tactic:
← Set.univ_inter {ω | τ ω = i},

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet (Set.univ ∩ {ω | τ ω = ↑i})
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 τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ ω ∈ {ω | ↑i ≤ τ ω} ↔ ω ∈ {ω | τ ω = ↑i} ∪ {ω | ↑i < τ ω}

Tactic:
simp only [le_iff_lt_or_eq, Set.mem_ofPred_eq, Set.mem_union]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ ↑i < τ ω ∨ ↑i = τ ω ↔ τ ω = ↑i ∨ ↑i < τ ω
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ log (μ.real Set.univ) + log (rexp (t * c)) = log (μ.real Set.univ) + t * c

pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ μ.real Set.univ ≠ 0

Tactic:
· rw [log_exp _]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ μ.real Set.univ ≠ 0
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
hπ : ∀ (ω : Ω), ↑(π ω) ≠ ∞
ω : Ω
h_le' : untopA (τ ω) ≤ untopA (π ω)
⊢ (stoppedValue u π - stoppedValue u τ) ω =
    (u (untopA (π ω)) - u 0 - ∑ k ∈ Finset.range (untopA (τ ω)), (u (k + 1) - u k)) ω

Tactic:
Finset.sum_range_sub

Goal state after:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
hπ : ∀ (ω : Ω), ↑(π ω) ≠ ∞
ω : Ω
h_le' : untopA (τ ω) ≤ untopA (π ω)
⊢ (stoppedValue u π - stoppedValue u τ) ω = (u (untopA (π ω)) - u 0 - (u (untopA (τ ω)) - u 0)) ω
Module: Mathlib.Probability.Moments.Basic

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

Tactic:
rw [show ⇑L = ⇑L.toHomeomorph.toMeasurableEquiv from rfl, integral_map_equiv]
  simp [L.integral_comp_id_comm]

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

Goal state before:
pp: case refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
ω : Ω
n : ℕ
⊢ process s n ω ≤ process s (n + 1) ω

Tactic:
rw [process, process, ← sub_nonneg, Finset.sum_apply, Finset.sum_apply,
      Finset.sum_range_succ_sub_sum]

Goal state after:
case refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
ω : Ω
n : ℕ
⊢ 0 ≤ (s (n + 1)).indicator 1 ω
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
x : E
⊢ ((covarianceBilin μ) x) x = Var[fun u ↦ ⟪x, u⟫; μ]

Tactic:
by
  rw [covarianceBilin_eq_covarianceBilinDual, covarianceBilinDual_self_eq_variance h]
  rfl

Goal state after:
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
this : b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2
⊢ (‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2) / √2 = (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2

Tactic:
field_simp; rw [Real.sq_sqrt (by positivity)]; ring

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

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

Tactic:
gcongr
      positivity

Goal state after:
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 μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
ha : ¬μ {x | ‖x‖ ≤ a} = 1
ha_lt : μ {x | ‖x‖ ≤ a} < 1
hc'_lt : c' < 1
x : E
ha' : a < ‖x‖
⊢ ‖x‖ ≤ a ∨ ∃ i, t i < ‖x‖ ∧ ‖x‖ ≤ t (i + 1)

Tactic:
exact Or.inr <| (normThreshold_strictMono ha_pos).exists_between_of_tendsto_atTop
        (tendsto_normThreshold_atTop ha_pos) ha'

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), AEMeasurable (X i) (⇑κ ∘ₘ P)
hY : AEMeasurable Y (⇑κ ∘ₘ P)
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
⊢ IndepFun (fun ω i ↦ X i ω) (AEMeasurable.mk Y hY) κ P

Tactic:
apply process_congr_left (X := fun i ↦ (hX i).mk (X i))

Goal state after:
case h1
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), AEMeasurable (X i) (⇑κ ∘ₘ P)
hY : AEMeasurable Y (⇑κ ∘ₘ P)
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
⊢ IndepFun (fun ω i ↦ AEMeasurable.mk (X i) ⋯ ω) (AEMeasurable.mk Y hY) κ P

case h2
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), AEMeasurable (X i) (⇑κ ∘ₘ P)
hY : AEMeasurable Y (⇑κ ∘ₘ P)
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
⊢ ∀ (i : S), ∀ᵐ (a : α) ∂P, AEMeasurable.mk (X i) ⋯ =ᵐ[κ a] X i
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess

Goal state before:
pp: T : Type u_1
inst✝¹ : LinearOrder T
I : Finset T
inst✝ : OrderBot T
⊢ Monotone I.orderEmbOfFinWithBot

Tactic:
intro i j hij
  obtain rfl | hi := eq_or_ne i 0
  · simp
  rw [orderEmbOfFinWithBot_of_ne_zero I i hi, orderEmbOfFinWithBot_of_ne_zero I j (by grind)]
  exact OrderEmbedding.monotone _ (by simpa)

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
this : Nonempty { r' // y < ↑r' }
⊢ ⨅ q, f a ↑q ≤ ⨅ q, f a ↑q

Tactic:
refine le_ciInf fun r ↦ (ciInf_le ?_ ?_).trans_eq ?_

Goal state after:
case refine_1
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
this : Nonempty { r' // y < ↑r' }
r : { q' // y < ↑q' }
⊢ BddBelow (range fun q ↦ f a ↑q)

case refine_2
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
this : Nonempty { r' // y < ↑r' }
r : { q' // y < ↑q' }
⊢ { q' // x < ↑q' }

case refine_3
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
this : Nonempty { r' // y < ↑r' }
r : { q' // y < ↑q' }
⊢ f a ↑?refine_2 = f a ↑r
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
⊢ MemLp (B (t i.succ)) 2 P

Tactic:
exact (hB.isGaussianProcess.hasGaussianLaw_eval _).memLp_two

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

Goal state before:
pp: case hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
⊢ MemLp (B (t i.castSucc)) 2 P

Tactic:
exact (hB.isGaussianProcess.hasGaussianLaw_eval _).memLp_two

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

Goal state before:
pp: case hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
⊢ MemLp (B (t j.succ)) 2 P

Tactic:
exact (hB.isGaussianProcess.hasGaussianLaw_eval _).memLp_two

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

Goal state before:
pp: case hT
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
⊢ MemLp (B (t j.castSucc)) 2 P

Tactic:
exact (hB.isGaussianProcess.hasGaussianLaw_eval _).memLp_two

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 : ℝ
⊢ Integrable (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) (ν a)

Tactic:
have : (fun b ↦ stieltjesOfMeasurableRat f hf.measurable (a, b) x)
      = fun b ↦ (ENNReal.ofReal (stieltjesOfMeasurableRat f hf.measurable (a, b) x)).toReal := by
    ext t
    rw [ENNReal.toReal_ofReal]
    exact stieltjesOfMeasurableRat_nonneg _ _ _

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) = fun b ↦
    (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal
⊢ Integrable (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) (ν a)
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case refine_2.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝¹ : Finite ι
κ : ι → Type u_4
inst✝ : ∀ (i : ι), Finite (κ i)
X : (i : ι) → κ i → Ω → ℝ
hX : HasGaussianLaw (fun ω i j ↦ X i j ω) P
h : ∀ (i j : ι), i ≠ j → ∀ (k : κ i) (l : κ j), cov[X i k, X j l; P] = 0
this✝² : IsProbabilityMeasure P
this✝¹ : (fun i ω j ↦ X i j ω) = fun i ↦ ofLp ∘ toLp 2 ∘ fun ω j ↦ X i j ω
this✝ : (i : ι) → Fintype (κ i) := fun i ↦ Fintype.ofFinite (κ i)
this : Fintype ι := Fintype.ofFinite ι
i j : ι
hij : i ≠ j
x : WithLp 2 (κ i → ℝ)
y : WithLp 2 (κ j → ℝ)
⊢ ∀ (i_1 : κ i),
    MemLp
      (fun ω ↦
        (starRingEnd ℝ) (((EuclideanSpace.basisFun (κ i) ℝ).repr x).ofLp i_1) *
          ⟪(EuclideanSpace.basisFun (κ i) ℝ) i_1, (toLp 2 ∘ fun ω j ↦ X i j ω) ω⟫)
      2 P

Tactic:
simpa using fun j ↦ ((hX.eval i).eval j).memLp_two.const_mul _

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

Goal state before:
pp: case refine_2.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
⊢ MemLp (B t₀) 2 P

Tactic:
exact (hB.isGaussianProcess.hasGaussianLaw_eval _).memLp_two

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

Goal state before:
pp: case refine_2.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
⊢ MemLp (B (t₀ + t)) 2 P

Tactic:
exact (hB.isGaussianProcess.hasGaussianLaw_eval _).memLp_two

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

Goal state before:
pp: case refine_2.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
⊢ MemLp (B t₀) 2 P

Tactic:
exact (hB.isGaussianProcess.hasGaussianLaw_eval _).memLp_two

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

Goal state before:
pp: case refine_2.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
⊢ MemLp (B (t₀ + s)) 2 P

Tactic:
exact (hB.isGaussianProcess.hasGaussianLaw_eval _).memLp_two

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

Goal state before:
pp: case refine_2.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
⊢ MemLp (B t₀) 2 P

Tactic:
exact (hB.isGaussianProcess.hasGaussianLaw_eval _).memLp_two

Goal state after: