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

Goal state before:
pp: case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = (fun x ↦ μ.real (s (n + 1))) ω
ω : Ω
hω : ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
B : ℝ
n : ℕ
hB : (∑ k ∈ Finset.range n, μ (s (k + 1))).toReal ≤ B
⊢ ¬↑B.toNNReal < ∑ k ∈ Finset.range n, μ (s (k + 1))

Tactic:
· rwa [not_lt, ENNReal.ofNNReal_toNNReal, ENNReal.le_ofReal_iff_toReal_le]
      · simp
      · exact le_trans (by positivity) hB

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝¹ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
⊢ stoppedValue u τ = ∑ i ∈ s, {ω | τ ω = ↑i}.indicator (u i)

Tactic:
by
  ext y
  classical
  rw [stoppedValue, Finset.sum_apply, Finset.sum_indicator_eq_sum_filter]
  suffices {i ∈ s | y ∈ {ω : Ω | τ ω = (i : ι)}} = ({(τ y).untopA} : Finset ι) by
    rw [this, Finset.sum_singleton]
  ext1 ω
  simp only [Set.mem_ofPred_eq, Finset.mem_filter, Finset.mem_singleton]
  constructor <;> intro h
  · simp [h.2]
  · simp only [h]
    specialize hbdd y
    have : τ y ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at hbdd
    lift τ y to ι using this with i hi
    simpa using hbdd

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

Goal state before:
pp: case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω ↦ rexp (a * X ω)) μ
hb : Integrable (fun ω ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) μ

Tactic:
by_cases hab : a = b

Goal state after:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω ↦ rexp (a * X ω)) μ
hb : Integrable (fun ω ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : a = b
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) μ

case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω ↦ rexp (a * X ω)) μ
hb : Integrable (fun ω ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
hab : ¬a = b
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : u ≤ 0
⊢ Integrable (fun ω ↦ rexp (|u| * X ω)) μ

Tactic:
· rwa [abs_of_nonpos hu]

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᵐ[ℙ] gaussianPDFReal μ v
⊢ (√(2 * π * ↑v))⁻¹ * ∫ (a : ℝ), rexp (-(a - μ) ^ 2 / (2 * ↑v)) = 1

Tactic:
rw [integral_sub_right_eq_self (μ := volume) (fun a ↦ rexp (-a ^ 2 / ((2 : ℝ) * v))) μ]

Goal state after:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᵐ[ℙ] gaussianPDFReal μ v
⊢ (√(2 * π * ↑v))⁻¹ * ∫ (x : ℝ), rexp (-x ^ 2 / (2 * ↑v)) = 1
Module: Mathlib.Probability.Moments.IntegrableExpMul

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

Tactic:
by
  refine (rpow_abs_le_mul_max_exp_of_pos x hp (t := |t|) ?_).trans_eq ?_
  · simp [ht]
  · congr
    rcases le_total 0 x with hx | hx
    · rw [abs_of_nonneg hx]
      simp only [neg_mul, sup_eq_left, exp_le_exp, neg_le_self_iff]
      positivity
    · rw [abs_of_nonpos hx]
      simp only [neg_mul, mul_neg, sup_eq_right, exp_le_exp, le_neg_self_iff]
      exact mul_nonpos_of_nonneg_of_nonpos (abs_nonneg _) hx

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

Goal state before:
pp: case refine_2.refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
h : Integrable (fun ω ↦ |X ω| ^ p * rexp (v * X ω)) μ
⊢ ∀ᵐ (a : Ω) ∂μ, ‖|X a ^ p| * rexp (v * X a)‖ ≤ |X a| ^ p * rexp (v * X a)

Tactic:
refine ae_of_all _ fun ω ↦ ?_

Goal state after:
case refine_2.refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
h : Integrable (fun ω ↦ |X ω| ^ p * rexp (v * X ω)) μ
ω : Ω
⊢ ‖|X ω ^ p| * rexp (v * X ω)‖ ≤ |X ω| ^ p * rexp (v * X ω)
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ (∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun u ↦ ∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ deriv (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v / (mgf X μ v * mgf X μ v) =
    deriv (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v

Tactic:
div_mul_eq_div_div,

Goal state after:
case e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ (∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun u ↦ ∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ deriv (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v / mgf X μ v / mgf X μ v =
    deriv (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ ∀ᵐ (a : Ω) ∂μ, ‖‖X a ^ p‖ * rexp (z.re * X a)‖ ≤ ‖|X a| ^ p * rexp (z.re * X a)‖

Tactic:
refine ae_of_all _ fun ω ↦ ?_

Goal state after:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
ω : Ω
⊢ ‖‖X ω ^ p‖ * rexp (z.re * X ω)‖ ≤ ‖|X ω| ^ p * rexp (z.re * X ω)‖
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: μ : Measure ℝ
h : IsGaussian μ
⊢ Measure.map (⇑(ContinuousLinearMap.id ℝ ℝ)) μ = gaussianReal (∫ (x : ℝ), id x ∂μ) Var[id; μ].toNNReal

Tactic:
by rw [h.map_eq_gaussianReal]; simp

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

Goal state before:
pp: case e_a.e_a.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ ∫ (a : Ω), 2 * (X a * rexp (v * X a)) * deriv (cgf X μ) v ∂μ =
    ∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ

Tactic:
congr with ω

Goal state after:
case e_a.e_a.e_a.e_f
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
ω : Ω
⊢ 2 * (X ω * rexp (v * X ω)) * deriv (cgf X μ) v = 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)
Module: Mathlib.Probability.Moments.MGFAnalytic

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

Tactic:
congr with ω

Goal state after:
case e_a.e_f
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
ω : Ω
⊢ (X ω ^ 2 - 2 * X ω * deriv (cgf X μ) v + deriv (cgf X μ) v ^ 2) * rexp (v * X ω) =
    (X ω - deriv (cgf X μ) v) ^ 2 * rexp (v * X ω)
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
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
n : ℕ
hn : μ {x | normThreshold a n < ‖x‖} ≤ μ {x | ‖x‖ ≤ a} * ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ n
h_mul_le : c * μ {x | normThreshold a (n + 1) < ‖x‖} ≤ μ {x | normThreshold a n < ‖x‖} ^ 2
⊢ c⁻¹ * (c * ((1 - c) / c) ^ 2 ^ n) ^ 2 = c * ((1 - c) / c) ^ 2 ^ (n + 1)

Tactic:
rw [mul_pow, ← pow_mul, ← mul_assoc, pow_two, ← mul_assoc,
        ENNReal.inv_mul_cancel hc_pos.ne' hc_lt_top.ne, one_mul, pow_add, pow_one]

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
C C' : ℝ
hint : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
y : E
hy : Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
⊢ rexp (C' * ‖x‖ ^ 2) ≤ rexp (C / ε * ‖y‖ ^ 2) * rexp (C * ‖x - y‖ ^ 2)

Tactic:
← Real.exp_add

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
C C' : ℝ
hint : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
y : E
hy : Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
⊢ rexp (C' * ‖x‖ ^ 2) ≤ rexp (C / ε * ‖y‖ ^ 2 + C * ‖x - y‖ ^ 2)
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
L : StrongDual ℝ E
⊢ charFunDual (stdGaussian E) L = cexp (-↑‖L‖ ^ 2 / 2)

Tactic:
by
  simp [IsGaussian.charFunDual_eq, integral_complex_ofReal, variance_dual_stdGaussian, neg_div]

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
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 : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c * a⁻¹ ^ 2
⊢ c *
      ENNReal.ofReal
        (rexp (2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n) * rexp (-Real.log (c / (1 - c)).toReal * 2 ^ n)) =
    c * ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * 2 ^ n))

Tactic:
← Real.exp_add

Goal state after:
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 : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c * a⁻¹ ^ 2
⊢ c *
      ENNReal.ofReal
        (rexp (2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n + -Real.log (c / (1 - c)).toReal * 2 ^ n)) =
    c * ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * 2 ^ n))
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s : ↥I
⊢ ∫ (x : ↥I → ℝ), (ContinuousLinearMap.proj s) x ∂projectiveFamily I = 0

Tactic:
ContinuousLinearMap.integral_comp_id_comm,

Goal state after:
I : Finset ℝ≥0
s : ↥I
⊢ (ContinuousLinearMap.proj s) (∫ (x : ↥I → ℝ), x ∂projectiveFamily I) = 0

case h
I : Finset ℝ≥0
s : ↥I
⊢ Integrable id (projectiveFamily I)
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x : EuclideanSpace ℝ ι
⊢ charFun (multivariateGaussian μ S) x = cexp (↑⟪x, μ⟫ * I - ↑(x.ofLp ⬝ᵥ S *ᵥ x.ofLp) / 2)

Tactic:
simp [IsGaussian.charFun_eq', covarianceBilin_multivariateGaussian hS]

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

Goal state before:
pp: case e_v
I : Finset ℝ≥0
s t : ↥I
⊢ (↑(↑s + ↑t) - ↑(2 * min ↑s ↑t)).toNNReal = nndist ↑s ↑t

Tactic:
← NNReal.coe_sub,

Goal state after:
case e_v
I : Finset ℝ≥0
s t : ↥I
⊢ (↑(↑s + ↑t - 2 * min ↑s ↑t)).toNNReal = nndist ↑s ↑t

case e_v
I : Finset ℝ≥0
s t : ↥I
⊢ 2 * min ↑s ↑t ≤ ↑s + ↑t
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s t : ↥I
⊢ gaussianReal (∫ (a : ↥I → ℝ), a s ∂projectiveFamily I - ∫ (a : ↥I → ℝ), a t ∂projectiveFamily I)
      (↑↑s - 2 * ↑(min ↑s ↑t) + ↑↑t).toNNReal =
    gaussianReal 0 (nndist ↑s ↑t)

pp: case hf
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x s) (projectiveFamily I)

pp: case hg
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x t) (projectiveFamily I)

pp: case hX
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x s) 2 (projectiveFamily I)

pp: case hY
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x t) 2 (projectiveFamily I)

pp: I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)

Tactic:
· congr
      · simp
      norm_cast
      rw [sub_add_eq_add_sub, ← NNReal.coe_add, ← NNReal.coe_sub, Real.toNNReal_coe]
      · wlog hst : (s : ℝ≥0) ≤ t generalizing s t
        · convert this t s (le_of_not_ge hst) using 1
          · rw [add_comm, min_comm]
          · rw [nndist_comm]
        grw [min_eq_left hst, NNReal.nndist_eq, max_eq_right (by grw [hst]), two_mul,
          add_tsub_add_eq_tsub_left]
      nth_grw 1 [two_mul, min_le_left, min_le_right]

Goal state after:
case hf
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x s) (projectiveFamily I)

case hg
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x t) (projectiveFamily I)

case hX
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x s) 2 (projectiveFamily I)

case hY
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x t) 2 (projectiveFamily I)

I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)
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
I : Finset T
⊢ HasGaussianLaw (fun ω ↦ ∑ i ∈ I, X i ω) P

Tactic:
convert! hX.hasGaussianLaw_sum (I := I)

Goal state after:
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
I : Finset T
x✝ : Ω
⊢ ∑ i ∈ I, X i x✝ = (∑ i ∈ I, X i) x✝
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 : Type u_5
𝓧 : S → Type u_6
𝓨 : T → Type u_7
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), Measurable (X i)
hY : ∀ (j : T), Measurable (Y j)
h : ∀ (I : Finset S) (J : Finset T), IndepFun (fun ω i ↦ X (↑i) ω) (fun ω j ↦ Y (↑j) ω) κ P
inst✝ : IsZeroOrMarkovKernel κ
⊢ IndepFun (fun ω i ↦ X i ω) (fun ω j ↦ Y j ω) κ P

Tactic:
by
  refine IndepFun.process_indepFun hX (measurable_pi_lambda _ hY) fun I ↦ ?_
  exact IndepFun.indepFun_process (measurable_pi_lambda _ fun _ ↦ hX _) hY fun J ↦ h I J

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 α
T : Type u_5
𝓧 : S → Type u_6
𝓨 : T → Type u_7
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), AEMeasurable (X i) (⇑κ ∘ₘ P)
hY : ∀ (j : T), AEMeasurable (Y j) (⇑κ ∘ₘ P)
h : ∀ (I : Finset S) (J : Finset T), IndepFun (fun ω i ↦ X (↑i) ω) (fun ω j ↦ Y (↑j) ω) κ P
inst✝ : IsZeroOrMarkovKernel κ
⊢ IndepFun (fun ω i ↦ AEMeasurable.mk (X i) ⋯ ω) (fun ω j ↦ AEMeasurable.mk (Y j) ⋯ ω) κ P

Tactic:
refine process_indepFun_process
    (fun i ↦ (hX i).measurable_mk) (fun j ↦ (hY j).measurable_mk) fun I J ↦ ?_

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

Goal state before:
pp: T : Type u_1
inst✝¹ : LinearOrder T
I : Finset T
inst✝ : Bot T
i : Fin #I
⊢ I.orderEmbOfFinWithBot i.succ = (I.orderEmbOfFin ⋯) i

Tactic:
rw [orderEmbOfFinWithBot_of_ne_zero, Fin.pred_succ]

Goal state after:
case hi
T : Type u_1
inst✝¹ : LinearOrder T
I : Finset T
inst✝ : Bot T
i : Fin #I
⊢ i.succ ≠ 0
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case e_f
α : 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 : β
⊢ (stieltjesOfMeasurableRat f ⋯ (a, b)).measure (Iic x) = (stieltjesOfMeasurableRat f ⋯ (a, b)).measure (⋂ i, Iic ↑↑i)

pp: case e_f.hs
α : 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 : β
⊢ Monotone fun r ↦ Iic ↑↑r

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:
· congr with y : 1
      simp only [mem_Iic, mem_iInter, Subtype.forall]
      exact le_iff_forall_lt_rat_imp_le

Goal state after:
case e_f.hs
α : 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 : β
⊢ Monotone fun r ↦ Iic ↑↑r

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

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.BrownianMotion.Basic

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
⊢ iIndepFun (fun i ω ↦ (-B) (t i.succ) ω - (-B) (t i.castSucc) ω) P

Tactic:
convert (hB.hasIndepIncrements n t ht).comp (fun _ x ↦ -x) (by fun_prop)

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
x✝¹ : Fin n
x✝ : Ω
⊢ (-B) (t x✝¹.succ) x✝ - (-B) (t x✝¹.castSucc) x✝ = ((fun x ↦ -x) ∘ fun ω ↦ B (t x✝¹.succ) ω - B (t x✝¹.castSucc) ω) x✝
Module: Mathlib.Probability.CDF

Goal state before:
pp: μ : Measure ℝ
⊢ (cdf μ).measure univ = 1

Tactic:
simp only [StieltjesFunction.measure_univ _ (tendsto_cdf_atBot μ) (tendsto_cdf_atTop μ), sub_zero,
    ENNReal.ofReal_one]

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

Goal state before:
pp: case refine_2.refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ (fun c ↦ f (a, c) q) ≤ᵐ[ν a] fun t ↦ ⨅ r, f (a, t) ↑r

Tactic:
· filter_upwards [hf.mono a] with c h_mono using le_ciInf (fun r ↦ h_mono (le_of_lt r.prop))

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 : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) tᶜ ∂ν a =
    ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) univ - ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a

Tactic:
congr with x; rw [measure_compl ht (measure_ne_top (hf.toKernel f (a, x)) _)]

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

Goal state before:
pp: α : Type u_1
m✝ : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace ↑(memPartition t n)
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet {x | x ∈ s}

Tactic:
exact measurableSet_partitionFiltration_of_mem _ _ hs

Goal state after: