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

Goal state before:
pp: o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ 0 + type α = type α

Tactic:
simp only [show 0 = type PEmpty by rfl, ← type_lex_sum]

Goal state after:
o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ type (PEmpty.{u + 1} ⊕ₗ α) = type α
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ type α + 0 = type α

Tactic:
simp only [show 0 = type PEmpty by rfl, ← type_lex_sum]

Goal state after:
o : OrderType.{u}
α : Type u
x✝ : LinearOrder α
⊢ type (α ⊕ₗ PEmpty.{u + 1}) = type α
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
n : Nucleus X
a b : X
h : b ∈ range ⇑n
⊢ a ⇨ b ∈ range ⇑n

Tactic:
rw [mem_range, ← h, map_himp_apply] at *

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✝⁴ : TopologicalSpace β
u : ι → Ω → β
inst✝³ : MeasurableSpace ι
t : ι → Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : BorelSpace ι
inst✝ : PseudoMetrizableSpace ι
h : IsStronglyProgressive f u
ht : IsStronglyProgressive f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
⊢ IsStronglyProgressive 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_measurable ((ht i).measurable.subtype_mk.prodMk measurable_snd)

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

Goal state before:
pp: case mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
a : Ω
h : τ a = ↑i
⊢ τ a ≤ ↑i ∧ ∀ (x : Ω), τ x < ↑i → ¬τ a ≤ τ x

pp: case mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
a : Ω
h : τ a ≤ ↑i ∧ ∀ (x : Ω), τ x < ↑i → ¬τ a ≤ τ x
⊢ τ a = ↑i

Tactic:
· simp only [h, lt_iff_le_not_ge, le_refl, and_imp, imp_self, imp_true_iff, and_self_iff]

Goal state after:
case mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
a : Ω
h : τ a ≤ ↑i ∧ ∀ (x : Ω), τ x < ↑i → ¬τ a ≤ τ x
⊢ τ a = ↑i
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
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
hhpred : StronglyAdapted ℱ fun n ↦ h (n + 1)
this : IsStronglyPredictable ℱ g
hhmgle : Martingale h ℱ μ
ω : Ω
hω : (f n - martingalePart (f + g) ℱ μ n) ω = (f - martingalePart (f + g) ℱ μ) 0 ω
⊢ (f n - martingalePart (f + g) ℱ μ n) ω = 0 ω

Tactic:
rw [hω, Pi.sub_apply, martingalePart]

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✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
hhpred : StronglyAdapted ℱ fun n ↦ h (n + 1)
this : IsStronglyPredictable ℱ g
hhmgle : Martingale h ℱ μ
ω : Ω
hω : (f n - martingalePart (f + g) ℱ μ n) ω = (f - martingalePart (f + g) ℱ μ) 0 ω
⊢ (f 0 - ((f + g) 0 - predictablePart (f + g) ℱ μ 0)) ω = 0 ω
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case h
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun m ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω
i : ℕ
hi : i ∈ Finset.range (upcrossingsBefore a b f N ω)
⊢ b - a ≤
    stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (i + 1) ω)) ω -
      stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N i ω)) ω

Tactic:
refine le_sub_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab ?_

Goal state after:
case h
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun m ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω
i : ℕ
hi : i ∈ Finset.range (upcrossingsBefore a b f N ω)
⊢ i < upcrossingsBefore a b f N ω
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: case ht
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
hab : a < b
this : (∫⁻ (ω : Ω), upcrossings a b f ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
⊢ ENNReal.ofReal (b - a) ≠ ∞ ∨ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ ≠ ∞

Tactic:
left; finiteness

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

Goal state before:
pp: case refine_1
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁹ : LinearOrder ι
inst✝⁸ : MeasurableSpace ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : BorelSpace ι
inst✝³ : TopologicalSpace β
f : Filtration ι m
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω ↦ min (τ ω) ↑i)
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t = (⋃ n, stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ ↑(seq n)}) ∪ stoppedValue u τ ⁻¹' t ∩ {ω | τ ω = ⊤}
⊢ MeasurableSet (⋃ n, stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ ↑(seq n)})

pp: case refine_2
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁹ : LinearOrder ι
inst✝⁸ : MeasurableSpace ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : BorelSpace ι
inst✝³ : TopologicalSpace β
f : Filtration ι m
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω ↦ min (τ ω) ↑i)
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t = (⋃ n, stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ ↑(seq n)}) ∪ stoppedValue u τ ⁻¹' t ∩ {ω | τ ω = ⊤}
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω | τ ω = ⊤})

Tactic:
· exact MeasurableSet.iUnion fun i ↦ le_iSup f (seq i) _
      (measurableSet_preimage_stoppedValue_inter hf_prog hτ ht (seq i))

Goal state after:
case refine_2
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁹ : LinearOrder ι
inst✝⁸ : MeasurableSpace ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : BorelSpace ι
inst✝³ : TopologicalSpace β
f : Filtration ι m
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω ↦ min (τ ω) ↑i)
t : Set β
ht : MeasurableSet t
seq : ℕ → ι
h_seq_tendsto : Tendsto seq atTop atTop
this :
  stoppedValue u τ ⁻¹' t = (⋃ n, stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ ↑(seq n)}) ∪ stoppedValue u τ ⁻¹' t ∩ {ω | τ ω = ⊤}
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω | τ ω = ⊤})
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
s t : ℝ
h_meas : ∀ (t : ℝ), Measurable fun x ↦ rexp (t * x)
⊢ ((fun x ↦ rexp (s * x)) ∘ X) ⟂ᵢ[μ] (fun x ↦ rexp (t * x)) ∘ Y

Tactic:
exact IndepFun.comp h_indep (h_meas s) (h_meas t)

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
inst✝ : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
⊢ MemLp (stoppedProcess u τ n) p μ

Tactic:
refine memLp_stoppedProcess_of_mem_finset hτ hu n (s := Finset.Iic n) fun ω h => ?_

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
inst✝ : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
ω : Ω
h : τ ω < ↑n
⊢ τ ω ∈ WithTop.some '' ↑(Finset.Iic n)
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
h : Integrable id μ
L : E →L[𝕜] F
⊢ ∫ (x : E), L (id x) ∂μ = L (∫ (x : E), id x ∂μ)

Tactic:
rw [L.integral_comp_comm h]

Goal state after:
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
h : Integrable id μ
L : E →L[𝕜] F
⊢ ∫ (x : E), L x ∂μ = L (∫ (x : E), id x ∂μ)

Tactic:
by
  change ∫ x, L (id x) ∂μ = _
  rw [L.integral_comp_comm h]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
⊢ iteratedDeriv 2 (cgf X μ) v = (∫ (x : Ω), (fun ω ↦ X ω ^ 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2

Tactic:
rw [iteratedDeriv_succ, iteratedDeriv_one]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
⊢ deriv (deriv (cgf X μ)) v = (∫ (x : Ω), (fun ω ↦ X ω ^ 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : IsGaussian μ
this : (Measure.map (⇑0) μ) Set.univ = 1
⊢ μ Set.univ = 1

Tactic:
simpa [-FunLike.coe_zero,
      Measure.map_apply (by fun_prop : Measurable (0 : StrongDual ℝ E)) .univ] using this

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

Goal state before:
pp: m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
t : ℝ
⊢ cexp (↑t * ↑m₁ * Complex.I - ↑↑v₁ * ↑t ^ 2 / 2 + (↑t * ↑m₂ * Complex.I - ↑↑v₂ * ↑t ^ 2 / 2)) =
    cexp (↑t * ↑(m₁ + m₂) * Complex.I - ↑↑(v₁ + v₂) * ↑t ^ 2 / 2)

Tactic:
simp only [Complex.ofReal_add, NNReal.coe_add]

Goal state after:
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
t : ℝ
⊢ cexp (↑t * ↑m₁ * Complex.I - ↑↑v₁ * ↑t ^ 2 / 2 + (↑t * ↑m₂ * Complex.I - ↑↑v₂ * ↑t ^ 2 / 2)) =
    cexp (↑t * (↑m₁ + ↑m₂) * Complex.I - (↑↑v₁ + ↑↑v₂) * ↑t ^ 2 / 2)
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case pos
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
h_Lp : MemLp id p μ
hp : p = 0
⊢ ‖(toLpₗ μ p) L‖ ≤ ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
simp only [h_Lp, toLpₗ_apply, Lp.norm_toLp]
    simp [hp]

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case e_6.e'_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 : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
⊢ ‖(√2 / 2) • p.1 + (√2 / 2) • p.2‖ = ‖p.1 + p.2‖ / √2

Tactic:
rw [← smul_add, norm_smul, div_eq_inv_mul, div_eq_inv_mul, h_twos]

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: a : ℝ
ha_pos : 0 < a
⊢ a / (1 - √2) < a

Tactic:
calc a / (1 - √2)
  _ ≤ 0 := div_nonpos_of_nonneg_of_nonpos ha_pos.le (by simp)
  _ < a := ha_pos

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case e_a
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_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ (1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a} ≠ ∞

Tactic:
· exact ENNReal.div_ne_top (by finiteness) (lt_trans (by simp) ha_gt).ne'

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

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Fintype ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ IsGaussian (stdGaussian E)

Tactic:
by
  refine isGaussian_iff_gaussian_charFun.2 ⟨0, innerSL ℝ,
    LinearMap.BilinForm.isPosSemidef_iff.2 isPosSemidef_inner, ?_⟩
  simp [charFun_stdGaussian, neg_div, innerSL_apply_apply ℝ]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : T → Type u_4
X : (t : T) → S t → Ω → E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess (fun p ω ↦ X p.fst p.snd ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X t₁ s₁, ⇑L₂ ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S ↑i)
i j : ↥I
hij : i ≠ j
L₁ : StrongDual ℝ (↥(J i) → E)
L₂ : StrongDual ℝ (↥(J j) → E)
x✝ : Ω
⊢ (⇑L₁ ∘ fun ω k ↦ X (↑i) (↑k) ω) x✝ = (∑ k, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑i ↑k) x✝

Tactic:
simp [-ContinuousLinearMap.comp_apply, ← L₁.sum_comp_single]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst✝ : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X s, ⇑L₂ ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
L₁ : StrongDual ℝ (↥I → E)
L₂ : StrongDual ℝ (↥J → E)
x✝ : Ω
⊢ (⇑L₁ ∘ fun ω i ↦ X (↑i) ω) x✝ = (∑ i, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun i ↦ E) i) ∘ X ↑i) x✝

Tactic:
simp [-ContinuousLinearMap.comp_apply, ← L₁.sum_comp_single]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
⊢ Measure.map (⇑(MeasurableEquiv.toLp 2 (↥I → ℝ))) (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P) =
    Measure.map (⇑(MeasurableEquiv.toLp 2 (↥I → ℝ))) (projectiveFamily I)

Tactic:
MeasurableEquiv.coe_toLp,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
⊢ Measure.map (WithLp.toLp 2) (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P) =
    Measure.map (WithLp.toLp 2) (projectiveFamily I)
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 α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), AEMeasurable (X i j) (⇑κ ∘ₘ P)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
⊢ iIndepFun (fun i ω j ↦ X i j ω) κ P

Tactic:
refine process_congr ?_ (fun i j ↦ Measure.ae_ae_of_ae_comp (hX i j).ae_eq_mk.symm)

Goal state after:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), AEMeasurable (X i j) (⇑κ ∘ₘ P)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
⊢ iIndepFun (fun i ω j ↦ AEMeasurable.mk (X i j) ⋯ ω) κ P
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
a : α
⊢ stieltjesOfMeasurableRat (fun p ↦ f p.2) ⋯ ((), a) = stieltjesOfMeasurableRat f hf a

Tactic:
stieltjesOfMeasurableRat,

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
a : α
⊢ ⋯.stieltjesFunction ((), a) = ⋯.stieltjesFunction a
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
this : ∀ (t : ℝ≥0) (ω : Ω), (√↑c)⁻¹ * B (c * t) ω = (√↑c)⁻¹ • (B ∘ fun x ↦ c * x) t ω
⊢ IsGaussianProcess (fun t ω ↦ (√↑c)⁻¹ • (B ∘ fun x ↦ c * x) t ω) P

Tactic:
exact (hB.isGaussianProcess.comp_right _).smul _

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
this :
  (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) - (1 + -((↑(√↑n)⁻¹ * ↑t) ^ 2 / 2))) =o[atTop] fun n ↦
    ((√↑n)⁻¹ * t) ^ 2
aux : (fun n ↦ ‖1 / ↑n‖) = fun n ↦ ‖1 / ↑n‖
⊢ (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) - (1 + -↑t ^ 2 / 2 / ↑n)) =o[atTop] fun n ↦ ‖1 / ↑n‖

Tactic:
Asymptotics.isLittleO_norm_right

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
this :
  (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) - (1 + -((↑(√↑n)⁻¹ * ↑t) ^ 2 / 2))) =o[atTop] fun n ↦
    ((√↑n)⁻¹ * t) ^ 2
aux : (fun n ↦ ‖1 / ↑n‖) = fun n ↦ ‖1 / ↑n‖
⊢ (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) - (1 + -↑t ^ 2 / 2 / ↑n)) =o[atTop] fun n ↦ 1 / ↑n
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: case inl
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
mX : ∀ (n : ℕ), AEMeasurable (X n) P
⊢ TendstoInDistribution (fun n ω ↦ (√↑n)⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P)) atTop Y
    (fun x ↦ P) P'

Tactic:
refine tendstoInDistribution_of_identDistrib 0 (fun n ↦ ?_) ?_

Goal state after:
case inl.refine_1
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
mX : ∀ (n : ℕ), AEMeasurable (X n) P
n : ℕ
⊢ IdentDistrib (fun ω ↦ (√↑0)⁻¹ * (∑ k ∈ Finset.range 0, X k ω - ↑0 * ∫ (x : Ω), X 0 x ∂P))
    (fun ω ↦ (√↑n)⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P)) P P

case inl.refine_2
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
mX : ∀ (n : ℕ), AEMeasurable (X n) P
⊢ IdentDistrib (fun ω ↦ (√↑0)⁻¹ * (∑ k ∈ Finset.range 0, X k ω - ↑0 * ∫ (x : Ω), X 0 x ∂P)) Y P P'
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : ↑S ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ ↑S)
⊢ ∫ (x : γ) in ⋃ i, ↑i, κ.densityProcess ν n a x s ∂ν a = (κ a).real ((⋃ i, ↑i) ×ˢ s)

Tactic:
have h_disj : Pairwise (Disjoint on fun i : S ↦ (i : Set γ)) := by
    intro u v huv
    simp only [Function.onFun]
    refine disjoint_countablePartition (hS_subset (by simp)) (hS_subset (by simp)) ?_
    rwa [ne_eq, ← Subtype.ext_iff]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : ↑S ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ ↑S)
h_disj : Pairwise (Disjoint on fun i ↦ ↑i)
⊢ ∫ (x : γ) in ⋃ i, ↑i, κ.densityProcess ν n a x s ∂ν a = (κ a).real ((⋃ i, ↑i) ×ˢ s)