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

Goal state before:
pp: case inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : ConditionallyCompleteLinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : Countable ι
x✝ : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
hi : i < n'
h_set_eq_Union : {ω | hittingBtwn u s n n' ω ≤ i} = ⋃ j ∈ Set.Icc n i, u j ⁻¹' s
⊢ MeasurableSet {ω | (fun ω ↦ ↑(hittingBtwn u s n n' ω)) ω ≤ ↑i}

Tactic:
simpa [h_set_eq_Union] using MeasurableSet.iUnion fun j =>
      MeasurableSet.iUnion fun hj => f.mono hj.2 _ ((hu j) hs)

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

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)

Tactic:
rw [ae_all_iff]

Goal state after:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ (i : ℕ), ∀ᵐ (a : Ω) ∂μ, ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n a) atTop (𝓝 c)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
h_min_eq_left : (fun x ↦ min (↑↑(↑x).1) (τ (↑x).2)) = fun x ↦ ↑↑(↑x).1
⊢ Measurable (sᶜ.domRestrict fun p ↦ min (↑↑p.1) (τ p.2))

Tactic:
by
      simp +unfoldPartialApp only [sc, Set.domRestrict, h_min_eq_left]
      exact (h_meas_fst _).withTop_coe

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

Goal state before:
pp: case neg
Ω : 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
ω : Ω
a✝ : stoppedValue u τ ω ∈ t
h : ¬τ ω = ⊤
⊢ (∃ x, τ ω ≤ ↑(seq x)) ∨ τ ω = ⊤

Tactic:
lift τ ω to ι using h with t

Goal state after:
case neg
Ω : 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
ω : Ω
a✝ : stoppedValue u τ ω ∈ t✝
t : ι
⊢ (∃ x, ↑t ≤ ↑(seq x)) ∨ ↑t = ⊤
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
s : Set Ω
inst✝¹ : DecidablePred fun x ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst✝ : Nonempty ι'
i j : ι'
f : ι' → Ω → α
⊢ stoppedValue f (s.piecewise (fun x ↦ ↑i) fun x ↦ ↑j) = s.piecewise (f i) (f j)

Tactic:
ext ω; rw [stoppedValue]; by_cases hx : ω ∈ s <;> simp [hx]

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

Goal state before:
pp: Ω : Type u_1
s : Set Ω
inst✝² : DecidablePred fun x ↦ x ∈ s
ι' : Type u_4
α : Type u_5
inst✝¹ : AddCommGroup α
inst✝ : Nonempty ι'
i j : ι'
f : ι' → Ω → α
⊢ stoppedValue f (s.piecewise (fun x ↦ ↑i) fun x ↦ ↑j) = s.indicator (f i) + sᶜ.indicator (f j)

Tactic:
ext ω; rw [stoppedValue]; by_cases hx : ω ∈ s <;> simp [hx]

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

Goal state before:
pp: m : ℝ
⊢ gaussianPDFReal m 0 = 0

Tactic:
ext1 x
  simp [gaussianPDFReal]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
⊢ HasFPowerSeriesAt (mgf X μ)
    (FormalMultilinearSeries.ofScalars ℝ fun n ↦ (∫ (x : Ω), (fun ω ↦ X ω ^ n * rexp (v * X ω)) x ∂μ) / ↑n !) v

Tactic:
by
  convert! (analyticAt_mgf hv).hasFPowerSeriesAt
  rw [iteratedDeriv_mgf hv]

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : v ≠ 0
f : ℝ ≃ᵐ ℝ
f' : ℝ → ℝ
h_deriv : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x
s : Set ℝ
hs : MeasurableSet s
⊢ (Measure.map (⇑f.symm) (gaussianReal μ v)) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))

Tactic:
rw [gaussianReal_of_var_ne_zero _ hv, gaussianPDF_def]
  exact f.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul' hs h_deriv
    (ae_of_all _ (gaussianPDFReal_nonneg _ _)) (integrable_gaussianPDFReal _ _)

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]
  by_cases hμ : μ = 0
  · simp [hμ]
  have h_mem : ∀ᶠ y in 𝓝 v, y ∈ interior (integrableExpSet X μ) :=
    isOpen_interior.eventually_mem h
  have h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ μ[fun ω ↦ X ω * exp (u * X ω)] / mgf X μ u := by
    filter_upwards [h_mem] with u hu using deriv_cgf hu
  have h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun u ↦ μ[fun ω ↦ X ω * exp (u * X ω)] := by
    filter_upwards [h_mem] with u hu using deriv_mgf hu
  rw [h_d_cgf.deriv_eq]
  calc deriv (fun u ↦ (∫ ω, X ω * exp (u * X ω) ∂μ) / mgf X μ u) v
  _ = (deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v * mgf X μ v -
      (∫ ω, X ω * exp (v * X ω) ∂μ) * deriv (mgf X μ) v) / mgf X μ v ^ 2 := by
    rw [deriv_fun_div]
    · rw [h_d_mgf.symm.differentiableAt_iff, ← iteratedDeriv_one]
      exact differentiableAt_iteratedDeriv_mgf h 1
    · exact differentiableAt_mgf h
    · exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
  _ = (deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v * mgf X μ v -
      (∫ ω, X ω * exp (v * X ω) ∂μ) * ∫ ω, X ω * exp (v * X ω) ∂μ) / mgf X μ v ^ 2 := by
    rw [deriv_mgf h]
  _ = deriv (fun u ↦ ∫ ω, X ω * exp (u * X ω) ∂μ) v / mgf X μ v - deriv (cgf X μ) v ^ 2 := by
    rw [sub_div]
    congr 1
    · rw [pow_two, div_mul_eq_div_div, mul_div_assoc, div_self, mul_one]
      exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
    · rw [deriv_cgf h]
      ring
  _ = (∫ ω, (X ω) ^ 2 * exp (v * X ω) ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2 := by
    congr
    convert! (hasDerivAt_integral_pow_mul_exp_real h 1).deriv using 1
    simp

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

Goal state before:
pp: case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
⊢ Integrable (fun ω ↦ rexp ((v - min (v - l) (u - v) / 2) * X ω)) μ

Tactic:
· exact h_subset (sub_half_inf_sub_mem_Ioo hvlu)

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
y : ℝ
⊢ Measure.map (fun x ↦ y - x) (gaussianReal μ v) = gaussianReal (y - μ) v

Tactic:
by
  simp_rw [sub_eq_add_neg]
  have : (fun x ↦ y + -x) = (fun x ↦ y + x) ∘ fun x ↦ -x := by ext; simp
  rw [this, ← Measure.map_map (by fun_prop) (by fun_prop), gaussianReal_map_neg,
    gaussianReal_map_const_add, add_comm]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : ∫ (x : Ω), X x ∂μ = 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
⊢ ∃ u ∈ Set.uIoo 0 t, cgf X μ t - 0 = iteratedDeriv 2 (cgf X μ) u * (t - 0) ^ 2 / 2

Tactic:
convert! taylor_mean_remainder_lagrange_iteratedDeriv ht.ne ?_

Goal state after:
case e'_2.e'_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : ∫ (x : Ω), X x ∂μ = 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x✝ : ℝ
⊢ 0 = taylorWithinEval (cgf X μ) 1 (Set.uIcc 0 t) 0 t

case convert_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : ∫ (x : Ω), X x ∂μ = 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
⊢ ContDiffOn ℝ (↑1 + 1) (cgf X μ) (Set.uIcc 0 t)
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case pos
μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x y : ℝ
h : MemLp id 2 μ
⊢ x * y * cov[fun u ↦ u, fun u ↦ u; μ] = x * y * Var[id; μ]

Tactic:
covariance_self aemeasurable_id',

Goal state after:
case pos
μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x y : ℝ
h : MemLp id 2 μ
⊢ x * y * Var[fun x ↦ x; μ] = x * y * Var[id; μ]
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: case e_a
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
⊢ Var[⇑((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E); μ] +
      Var[⇑((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E); μ] =
    Var[⇑(L ∘SL ContinuousLinearMap.inl ℝ E E); μ] + Var[⇑(L ∘SL ContinuousLinearMap.inr ℝ E E); μ]

Tactic:
have h1 : (L.comp (.rotation θ)).comp (.inl ℝ E E)
      = Real.cos θ • L.comp (.inl ℝ E E) - Real.sin θ • L.comp (.inr ℝ E E) := by
    ext x
    simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.inl_apply,
      ContinuousLinearMap.rotation_apply, smul_zero, add_zero]
    rw [← L.comp_inl_add_comp_inr]
    simp [-neg_smul, sub_eq_add_neg]

Goal state after:
case e_a
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
h1 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E =
    Real.cos θ • L ∘SL ContinuousLinearMap.inl ℝ E E - Real.sin θ • L ∘SL ContinuousLinearMap.inr ℝ E E
⊢ Var[⇑((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E); μ] +
      Var[⇑((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E); μ] =
    Var[⇑(L ∘SL ContinuousLinearMap.inl ℝ E E); μ] + Var[⇑(L ∘SL ContinuousLinearMap.inr ℝ E E); μ]
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ charFunDual μ L = cexp (↑(L (∫ (x : E), id x ∂μ)) * I - ↑(((covarianceBilinDual μ) L) L) / 2)

Tactic:
rw [IsGaussian.charFunDual_eq, covarianceBilinDual_self_eq_variance, integral_complex_ofReal,
    L.integral_comp_id_comm']
  · exact IsGaussian.integrable_id
  · exact IsGaussian.memLp_two_id

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
⊢ ‖c‖ = ‖y - (y - c)‖

Tactic:
by abel_nf

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✝ : ‖c‖ / 2 ≤ ‖y‖
⊢ ‖c‖ ^ ↑p = ‖c‖ ^ (↑p - 1 + 1)

Tactic:
by abel_nf

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsGaussian μ
t : E
⊢ charFun μ t = cexp (↑⟪t, ∫ (x : E), id x ∂μ⟫ * I - ↑(((covarianceBilin μ) t) t) / 2)

Tactic:
by
  rw [IsGaussian.charFun_eq, covarianceBilin_self, integral_complex_ofReal,
    integral_inner]
  · rfl
  · exact IsGaussian.integrable_id
  · exact IsGaussian.memLp_two_id

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this : ∀ (i : ι), (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫
⊢ ((covarianceBilin (multivariateGaussian μ S)) ((EuclideanSpace.basisFun ι ℝ) i)) ((EuclideanSpace.basisFun ι ℝ) j) =
    S i j

pp: case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this : ∀ (i : ι), (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫
⊢ MemLp id 2 (multivariateGaussian μ S)

Tactic:
covarianceBilin_multivariateGaussian hS

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this : ∀ (i : ι), (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫
⊢ ((EuclideanSpace.basisFun ι ℝ) i).ofLp ⬝ᵥ S *ᵥ ((EuclideanSpace.basisFun ι ℝ) j).ofLp = S i j

case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this : ∀ (i : ι), (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫
⊢ MemLp id 2 (multivariateGaussian μ S)
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
X : Ω → E
inst✝ : NormedSpace ℝ E
hX : HasGaussianLaw X P
⊢ HasGaussianLaw (-X) P

Tactic:
simpa using hX.smul (-1)

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

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
m : ℝ
x : ↥(image t univ) → E
x✝ : Fin n
⊢ m • x ⟨t x✝.succ, ⋯⟩ - m • x ⟨t x✝.castSucc, ⋯⟩ = m • (x ⟨t x✝.succ, ⋯⟩ - x ⟨t x✝.castSucc, ⋯⟩)

Tactic:
module

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

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : SecondCountableTopology E
inst✝ : Add T
h : IsGaussianProcess X P
t₀ t : T
c : ℝ
x : ↥{t₀, t₀ + t} → E
⊢ c • x ⟨t₀ + t, ⋯⟩ - c • x ⟨t₀, ⋯⟩ = c • (x ⟨t₀ + t, ⋯⟩ - x ⟨t₀, ⋯⟩)

Tactic:
module

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)
x y : ↥(I.sigma fun i ↦ if hi : i ∈ I then J ⟨i, hi⟩ else ∅) → E
⊢ (fun i j ↦ (x + y) ⟨⟨↑i, ↑j⟩, ⋯⟩) = (fun i j ↦ x ⟨⟨↑i, ↑j⟩, ⋯⟩) + fun i j ↦ y ⟨⟨↑i, ↑j⟩, ⋯⟩

Tactic:
ext; simp

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)
c : ℝ
x : ↥(I.sigma fun i ↦ if hi : i ∈ I then J ⟨i, hi⟩ else ∅) → E
⊢ (fun i j ↦ (c • x) ⟨⟨↑i, ↑j⟩, ⋯⟩) = (RingHom.id ℝ) c • fun i j ↦ x ⟨⟨↑i, ↑j⟩, ⋯⟩

Tactic:
ext; simp

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✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ¬∃ a, 0 < a ∧ 2⁻¹ < μ {x | ‖x‖ ≤ a} ∧ μ {x | ‖x‖ ≤ a} < 1
b : ℝ
hb : μ {x | ‖x‖ ≤ b} = 1
⊢ (fun x ↦ ‖x‖ ≤ b) ⁻¹' {True} = {x | ‖x‖ ≤ b}

Tactic:
ext; simp

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

Goal state before:
pp: case pos
x y : ℚ
hxy : x ≤ y
h_1 : x < 0
h_2 : y < 0
⊢ 0 ≤ 0

pp: case neg
x y : ℚ
hxy : x ≤ y
h_1 : x < 0
h_2 : ¬y < 0
⊢ 0 ≤ 1

pp: case pos
x y : ℚ
hxy : x ≤ y
h_1 : ¬x < 0
h_2 : y < 0
⊢ 1 ≤ 0

pp: case neg
x y : ℚ
hxy : x ≤ y
h_1 : ¬x < 0
h_2 : ¬y < 0
⊢ 1 ≤ 1

Tactic:
exacts [le_rfl, zero_le_one, absurd (hxy.trans_lt h_2) h_1, le_rfl]

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
⊢ ⨅ q, f a ↑q = ⨅ r_1, f a ↑r_1

Tactic:
refine Equiv.iInf_congr ?_ ?_

Goal state after:
case refine_1
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
⊢ { q' // ↑r < ↑q' } ≃ ↑(Ioi r)

case refine_2
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
⊢ ∀ (x : { q' // ↑r < ↑q' }), f a ↑(?refine_1 x) = f a ↑x
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case e_f.hsm
α : 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
hρ_zero : ¬(ν a).restrict s = 0
b : β
⊢ ∀ (i : { r' // x < ↑r' }), NullMeasurableSet (Iic ↑↑i) (stieltjesOfMeasurableRat f ⋯ (a, b)).measure

pp: case e_f.hfin
α : 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
hρ_zero : ¬(ν a).restrict s = 0
b : β
⊢ ∃ i, (stieltjesOfMeasurableRat f ⋯ (a, b)).measure (Iic ↑↑i) ≠ ∞

Tactic:
· exact fun _ ↦ nullMeasurableSet_Iic

Goal state after:
case e_f.hfin
α : 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
hρ_zero : ¬(ν a).restrict s = 0
b : β
⊢ ∃ i, (stieltjesOfMeasurableRat f ⋯ (a, b)).measure (Iic ↑↑i) ≠ ∞
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 : ℝ
⊢ ∫⁻ (x_1 : β) in univ, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, x_1)) x) ∂ν a = (κ a) (univ ×ˢ Iic x)

Tactic:
setLIntegral_stieltjesOfMeasurableRat hf _ _ MeasurableSet.univ

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
⊢ (κ a) (univ ×ˢ Iic x) = (κ a) (univ ×ˢ Iic x)
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, ∀ (r : ℚ), preCDF ρ r a ≤ 1

Tactic:
rw [ae_all_iff]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ ∀ (i : ℚ), ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ 1
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ ↑(Ioi q)

pp: case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ f (a, t) ↑?refine_2 ≤ 1

Tactic:
· exact ⟨q + 1, by simp⟩

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ f (a, t) ↑⟨q + 1, ⋯⟩ ≤ 1