mathlib-initiative/mathlib-tactics huggingface dataset:
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 ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R

Tactic:
simpa only [g, sub_sub_sub_cancel_right]

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

Goal state before:
pp: Ω : 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 ι
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
⊢ IsStronglyProgressive f (MeasureTheory.stoppedProcess u τ)

Tactic:
have h_meas := isStronglyProgressive_min_stopping_time hτ

Goal state after:
Ω : 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 ι
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_meas : IsStronglyProgressive f fun i ω ↦ (min (↑i) (τ ω)).untopA
⊢ IsStronglyProgressive f (MeasureTheory.stoppedProcess u τ)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case coe
Ω : 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 ι
h : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
h_meas : IsStronglyProgressive f fun i ω ↦ (min (↑i) (τ ω)).untopA
i : ι
ω : Ω
t : ι
⊢ (min ↑i ↑t).untopA ≤ i

Tactic:
rcases le_total i t with h_it | h_ti
    · simp [(mod_cast h_it : (i : WithTop ι) ≤ t)]
    · simpa [(mod_cast h_ti : t ≤ (i : WithTop ι))]

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

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ u i ω = {a | ↑n ≤ τ a}.indicator (u n) ω + {ω | τ ω = ↑i}.indicator (u i) ω

Tactic:
rw [Set.indicator_of_notMem, zero_add, Set.indicator_of_mem]

Goal state after:
case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ ω ∈ {ω | τ ω = ↑i}

case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ ω ∉ {a | ↑n ≤ τ a}
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω ↦ rexp (t * X i ω)) μ
⊢ Integrable (fun ω ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ

Tactic:
classical
  induction s using Finset.induction_on with
  | empty =>
    simp only [Finset.sum_apply, sum_empty, mul_zero, exp_zero]
    exact integrable_const _
  | insert i s hi_notin_s h_rec =>
    have : ∀ i : ι, i ∈ s → Integrable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
      h_int i (mem_insert_of_mem hi)
    specialize h_rec this
    rw [sum_insert hi_notin_s]
    refine IndepFun.integrable_exp_mul_add ?_ (h_int i (mem_insert_self _ _)) h_rec
    exact (h_indep.indepFun_finsetSum_of_notMem h_meas hi_notin_s).symm

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

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
u v : ℝ
huv : u ≠ v
hu_int : Integrable (fun ω ↦ rexp (u * X ω)) μ
hv_int : Integrable (fun ω ↦ rexp (v * X ω)) μ
hu : ¬u = 0
⊢ AEMeasurable X μ

Tactic:
exact aemeasurable_of_aemeasurable_exp_mul hu hu_int.aemeasurable

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

Goal state before:
pp: case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp (-t * X ω)) μ
⊢ Integrable (fun ω ↦ rexp ((0 + t) * X ω)) μ

Tactic:
simpa using ht_int_pos

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
ht_nonpos : t ≤ 0
⊢ Integrable (fun ω ↦ rexp ((v - -t) * X ω)) μ

Tactic:
simpa using ht_int_pos

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp (-t * X ω)) μ
ht_nonpos : t ≤ 0
⊢ Integrable (fun ω ↦ rexp (- -t * X ω)) μ

Tactic:
simpa using ht_int_pos

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

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

Tactic:
abs_of_nonpos ht_neg.le,

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

Goal state before:
pp: case refine_2.refine_3.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
h_le : ∀ (a : Ω), |X a| ^ p * rexp (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)
ω : Ω
⊢ |(p / (|t| - x)) ^ p| = (p / (|t| - x)) ^ p

Tactic:
simp only [abs_eq_self]

Goal state after:
case refine_2.refine_3.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
h_le : ∀ (a : Ω), |X a| ^ p * rexp (v * X a + x * |X a|) ≤ (p / (|t| - x)) ^ p * rexp (v * X a + |t| * |X a|)
ω : Ω
⊢ 0 ≤ (p / (|t| - x)) ^ p
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case refine_5.refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ Integrable (fun ω ↦ rexp ((z.re - t) * X ω)) μ

pp: case refine_5.refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ 0 ≤ t / 2

pp: case refine_5.refine_4
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ t / 2 < |t|

Tactic:
· exact h_subset (sub_half_inf_sub_mem_Ioo hlu)

Goal state after:
case refine_5.refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ 0 ≤ t / 2

case refine_5.refine_4
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ t / 2 < |t|
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω ↦ rexp ((0 + t) * X ω)) μ

Tactic:
simpa using ht_int_pos

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
⊢ AEMeasurable X μ

Tactic:
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hv
  obtain ⟨l, u, hvlu, h_subset⟩ := hv
  let t := ((v - l) ⊓ (u - v)) / 2
  have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hvlu.1, hvlu.2]
  have ht : 0 < t := half_pos h_pos
  by_cases hvt : v + t = 0
  · have hvt' : v - t ≠ 0 := by
      rw [sub_ne_zero]
      refine fun h_eq ↦ ht.ne' ?_
      simpa [h_eq] using hvt
    exact aemeasurable_of_aemeasurable_exp_mul hvt'
      (h_subset (sub_half_inf_sub_mem_Ioo hvlu)).aemeasurable
  · exact aemeasurable_of_aemeasurable_exp_mul hvt
      (h_subset (add_half_inf_sub_mem_Ioo hvlu)).aemeasurable

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

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

Tactic:
gaussianReal_map_add_const

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

Goal state before:
pp: case neg.refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')}
xs : ℕ → ℝ
hx_tendsto : Tendsto xs atTop (𝓝[≠] t)
hx_eq : ∀ (n : ℕ), complexMGF X μ ↑(xs n) = complexMGF Y μ' ↑(xs n)
⊢ Tendsto (fun n ↦ ↑(xs n)) atTop (𝓝[≠] ↑t)

Tactic:
rw [tendsto_nhdsWithin_iff] at hx_tendsto ⊢

Goal state after:
case neg.refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')}
xs : ℕ → ℝ
hx_tendsto : Tendsto xs atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, xs n ∈ {t}ᶜ
hx_eq : ∀ (n : ℕ), complexMGF X μ ↑(xs n) = complexMGF Y μ' ↑(xs n)
⊢ Tendsto (fun n ↦ ↑(xs n)) atTop (𝓝 ↑t) ∧ ∀ᶠ (n : ℕ) in atTop, ↑(xs n) ∈ {↑t}ᶜ
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
h : complexMGF X μ = complexMGF Y μ'
⊢ Measure.map X μ = Measure.map Y μ'

Tactic:
by
  have inner_ne_zero (x : ℝ) (h : x ≠ 0) : innerₗ ℝ x ≠ 0 :=
    DFunLike.ne_iff.mpr ⟨x, inner_self_ne_zero.mpr h⟩
  apply MeasureTheory.ext_of_integral_char_eq continuous_probChar probChar_ne_one inner_ne_zero
    continuous_inner (fun w ↦ ?_)
  rw [funext_iff] at h
  specialize h (Multiplicative.toAdd w * I)
  simp_rw [complexMGF, mul_assoc, mul_comm I, ← mul_assoc] at h
  simp only [BoundedContinuousFunction.char_apply, innerₗ_apply_apply,
    RCLike.inner_apply, conj_trivial, probChar_apply, ofReal_mul]
  rwa [integral_map hX (by fun_prop), integral_map hY (by fun_prop)]

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

Goal state before:
pp: ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ cov[fun u ↦ ⟪x, u⟫, fun u ↦ ⟪y, u⟫; Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ] =
    ∑ i, ∑ j, x.ofLp i * y.ofLp j * cov[X i, X j; μ]

pp: case h
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ MemLp id 2 (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)

Tactic:
covariance_map_fun,

Goal state after:
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ cov[fun ω ↦ ⟪x, toLp 2 fun x ↦ X x ω⟫, fun ω ↦ ⟪y, toLp 2 fun x ↦ X x ω⟫; μ] =
    ∑ i, ∑ j, x.ofLp i * y.ofLp j * cov[X i, X j; μ]

case hX
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEStronglyMeasurable (fun u ↦ ⟪x, u⟫) (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)

case hY
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEStronglyMeasurable (fun u ↦ ⟪y, u⟫) (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)

case hZ
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEMeasurable (fun ω ↦ toLp 2 fun x ↦ X x ω) μ

case h
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ MemLp id 2 (Measure.map (fun ω ↦ toLp 2 fun x ↦ X 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
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ μ {x | ‖x‖ ≤ a} * μ {x | b < ‖x‖} = (μ.prod μ) ({x | ‖x‖ ≤ a} ×ˢ {y | b < ‖y‖})

Tactic:
by rw [Measure.prod_prod]

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

Goal state before:
pp: case e_6
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)⁻¹
⊢ {a_1 | ‖(√2 / 2) • a_1.1 + -((√2 / 2) • a_1.2)‖ ≤ a ∧ b < ‖(√2 / 2) • a_1.1 + (√2 / 2) • a_1.2‖} =
    {p | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2}

Tactic:
congr! with p

Goal state after:
case e_6.e'_1
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

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
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:
by
  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 = nndist ↑s ↑t

Tactic:
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]

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

Goal state before:
pp: case refine_2
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h :
  ∀ (I : Finset T), Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P = Measure.map (fun ω ↦ I.restrict fun x ↦ Y x ω) P
⊢ Measure.map (fun ω x ↦ X x ω) P = Measure.map (fun ω x ↦ Y x ω) P

Tactic:
have hX' := isProjectiveLimit_map hX

Goal state after:
case refine_2
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h :
  ∀ (I : Finset T), Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P = Measure.map (fun ω ↦ I.restrict fun x ↦ Y x ω) P
hX' : IsProjectiveLimit (Measure.map (fun ω x ↦ X x ω) P) fun I ↦ Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P
⊢ Measure.map (fun ω x ↦ X x ω) P = Measure.map (fun ω x ↦ Y x ω) P
Module: Mathlib.Probability.Process.FiniteDimensionalLaws

Goal state before:
pp: case refine_4
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h : ∀ (I : Finset T), IdentDistrib (fun ω ↦ I.restrict fun x ↦ X x ω) (fun ω ↦ I.restrict fun x ↦ Y x ω) P P
⊢ Measure.map (fun ω x ↦ X x ω) P = Measure.map (fun ω x ↦ Y x ω) P

Tactic:
exact (map_eq_iff_forall_finset_map_restrict_eq hX hY).mpr (fun I ↦ (h I).map_eq)

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 Y : T → Ω → E
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module ℝ E
hX : IsGaussianProcess X P
hXY : ∀ (t : T), X t =ᵐ[P] Y t
I : Finset T
⊢ IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ Y x ω) P)

Tactic:
map_restrict_eq_of_forall_ae_eq fun t ↦ (hXY t).symm

Goal state after:
T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : T → Ω → E
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module ℝ E
hX : IsGaussianProcess X P
hXY : ∀ (t : T), X t =ᵐ[P] Y t
I : Finset T
⊢ IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
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 ↦ X i ω) (fun ω j ↦ Y j ω) κ P

Tactic:
by
  refine process_congr ?_ (fun i ↦ Measure.ae_ae_of_ae_comp (hX i).ae_eq_mk.symm)
    (fun j ↦ Measure.ae_ae_of_ae_comp (hY j).ae_eq_mk.symm)
  refine process_indepFun_process
    (fun i ↦ (hX i).measurable_mk) (fun j ↦ (hY j).measurable_mk) fun I J ↦ ?_
  exact process_congr (h I J) (fun i ↦ Measure.ae_ae_of_ae_comp (hX i).ae_eq_mk)
    (fun j ↦ Measure.ae_ae_of_ae_comp (hY j).ae_eq_mk)

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

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ ↑(-i)
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ ↑(- -i)
⊢ x.2 ≤ ↑i

pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ ↑i
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ ↑(-i)
⊢ x.2 ≤ ↑(-i)

Tactic:
· rw [neg_neg] at h'; exact h'.2

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r ↦ ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ ↑i
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ ↑(-i)
⊢ x.2 ≤ ↑(-i)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case neg
α : 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
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a =
    ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a
h_nonempty : Nonempty { r' // x < ↑r' }
⊢ (κ a) (⋂ i, s ×ˢ Iic ↑↑i) = (κ a) (s ×ˢ Iic x)

Tactic:
rw [← prod_iInter]

Goal state after:
case neg
α : 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
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a =
    ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a
h_nonempty : Nonempty { r' // x < ↑r' }
⊢ (κ a) (s ×ˢ ⋂ i, Iic ↑↑i) = (κ a) (s ×ˢ Iic x)