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

Goal state before:
pp: case refine_1
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ t₁ ≤ a • t₁ + b • t₂

Tactic:
simp only [smul_eq_mul]
    calc t₁
    _ = a * t₁ + b * t₁ := by rw [← add_mul, hab, one_mul]
    _ ≤ a * t₁ + b * t₂ := by gcongr

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
⊢ {a | ↑n ≤ τ a}.indicator (u n) x = {a | τ a = ↑n}.indicator (u n) x + {a | ↑n + 1 ≤ τ a}.indicator (u n) x

Tactic:
← Set.indicator_union_of_notMem_inter

Goal state after:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
⊢ {a | ↑n ≤ τ a}.indicator (u n) x = ({a | τ a = ↑n} ∪ {a | ↑n + 1 ≤ τ a}).indicator (u n) x

case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
⊢ x ∉ {a | τ a = ↑n} ∩ {a | ↑n + 1 ≤ τ a}
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n✝ : ℕ
h_re_of_mem :
  ∀ (n : ℕ),
    ∀ t ∈ interior (integrableExpSet X μ),
      (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
n : ℕ
⊢ ∀ᶠ (t' : ℝ) in 𝓝 t,
    (∫ (ω : Ω), ↑(X ω) ^ n * Complex.exp (↑t' * ↑(X ω)) ∂μ).re = ∫ (ω : Ω), X ω ^ n * rexp (t' * X ω) ∂μ

Tactic:
filter_upwards [isOpen_interior.eventually_mem ht] with t ht' using h_re_of_mem n t ht'

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    t ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
h_mem : ∀ᶠ (y : ℝ) in 𝓝 t, y ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (mgf X μ)) =ᶠ[𝓝 t] fun t ↦ ∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ

Tactic:
filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ Continuous (mgf X μ)

Tactic:
rw [← continuousOn_univ]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ ContinuousOn (mgf X μ) Set.univ
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
h_mem : ∀ᶠ (y : ℂ) in 𝓝 z, y.re ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun z ↦
    ∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ

Tactic:
filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst✝ : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
⊢ mgf X μ 0 ≠ 0

Tactic:
exact (mgf_pos (by simp)).ne'

Goal state after:
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 μ'
inner_ne_zero : ∀ (x : ℝ), x ≠ 0 → (innerₗ ℝ) x ≠ 0
w : ℝ
⊢ ∫ (v : ℝ), (BoundedContinuousFunction.char continuous_probChar ⋯ w) v ∂Measure.map X μ =
    ∫ (v : ℝ), (BoundedContinuousFunction.char continuous_probChar ⋯ w) v ∂Measure.map Y μ'

Tactic:
funext_iff

Goal state after:
Ω : 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 : ∀ (x : ℂ), complexMGF X μ x = complexMGF Y μ' x
inner_ne_zero : ∀ (x : ℝ), x ≠ 0 → (innerₗ ℝ) x ≠ 0
w : ℝ
⊢ ∫ (v : ℝ), (BoundedContinuousFunction.char continuous_probChar ⋯ w) v ∂Measure.map X μ =
    ∫ (v : ℝ), (BoundedContinuousFunction.char continuous_probChar ⋯ w) v ∂Measure.map Y μ'
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ integrableExpSet id (gaussianReal μ v) = Set.univ

Tactic:
ext
  simpa [integrableExpSet] using integrable_exp_mul_gaussianReal _

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ ↑((L 1 ^ 2).toNNReal * v) = ↑(L 1 ^ 2).toNNReal * ↑v

Tactic:
simp only [NNReal.coe_mul, Real.coe_toNNReal']

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 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ cov[(fun u ↦ ⟪(basisFun ι ℝ) i, u⟫) ∘ fun ω ↦ toLp 2 fun x ↦ X x ω,
      (fun u ↦ ⟪(basisFun ι ℝ) j, u⟫) ∘ fun ω ↦ toLp 2 fun x ↦ X x ω; μ] =
    cov[X i, X j; μ]

Tactic:
simp [basisFun_inner]; rfl

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

Goal state before:

Tactic:
∫⁻ x, ‖L x‖ₑ ^ p.toReal ∂μ
  _ ≤ ∫⁻ x, ‖L‖ₑ ^ p.toReal * ‖x‖ₑ ^ p.toReal ∂μ := by
    refine lintegral_mono fun x ↦ ?_
    rw [← ENNReal.mul_rpow_of_nonneg]
    swap; · positivity
    gcongr
    exact L.le_opENorm x
  _ = ‖L‖ₑ ^ p.toReal * ∫⁻ x, ‖x‖ₑ ^ p.toReal ∂μ := by rw [lintegral_const_mul]; fun_prop

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
⊢ Continuous[ContinuousLinearMap.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (toLpₗ μ p).toFun

Tactic:
by
    refine LinearMap.continuous_of_locally_bounded _ fun s hs ↦ ?_
    rw [image_isVonNBounded_iff]
    simp_rw [isVonNBounded_iff'] at hs
    obtain ⟨r, hxr⟩ := hs
    refine ⟨r * (eLpNorm id p μ).toReal, fun L hLs ↦ ?_⟩
    specialize hxr L hLs
    refine (StrongDual.norm_toLpₗ_le L).trans ?_
    gcongr

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 - 1) * ‖c‖ ≤ ‖c‖ ^ (↑p - 1) * (2 * ‖y‖)

Tactic:
gcongr; linarith

Goal state after:
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
this : (⇑L ∘ fun x ↦ ∑ i, x i • (stdOrthonormalBasis ℝ E) i) = ∑ i, fun x ↦ L ((stdOrthonormalBasis ℝ E) i) * x i
⊢ ∑ x, L ((stdOrthonormalBasis ℝ E) x) ^ 2 * Var[id; gaussianReal 0 1] = ‖L‖ ^ 2

Tactic:
variance_id_gaussianReal,

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
L : StrongDual ℝ E
this : (⇑L ∘ fun x ↦ ∑ i, x i • (stdOrthonormalBasis ℝ E) i) = ∑ i, fun x ↦ L ((stdOrthonormalBasis ℝ E) i) * x i
⊢ ∑ x, L ((stdOrthonormalBasis ℝ E) x) ^ 2 * ↑1 = ‖L‖ ^ 2
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
⊢ cexp ((∫ (x : E), ↑((fun x ↦ ⟪t, x⟫) x) ∂μ) * I - ↑Var[fun x ↦ ⟪t, x⟫; μ] / 2) =
    cexp (↑⟪t, ∫ (x : E), id x ∂μ⟫ * I - ↑(((covarianceBilin μ) t) t) / 2)

Tactic:
covarianceBilin_self,

Goal state after:
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
⊢ cexp ((∫ (x : E), ↑((fun x ↦ ⟪t, x⟫) x) ∂μ) * I - ↑Var[fun x ↦ ⟪t, x⟫; μ] / 2) =
    cexp (↑⟪t, ∫ (x : E), id x ∂μ⟫ * I - ↑Var[fun u ↦ ⟪t, u⟫; μ] / 2)

case h
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
⊢ MemLp id 2 μ
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable ⇑L
⊢ IsGaussian (Measure.map (⇑L ∘ X) P)

Tactic:
have := hX.isGaussian_map

Goal state after:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable ⇑L
this : IsGaussian (Measure.map X P)
⊢ IsGaussian (Measure.map (⇑L ∘ X) P)
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✝ : IsFiniteMeasure μ
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
g : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
  f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
    (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
⊢ ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((g L) L) / 2)

Tactic:
simp [← charFun_toDual_symm_eq_charFunDual, h, g]

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

Goal state before:
pp: I : Finset ℝ≥0
f : (↥I → ℝ) → ℝ
⊢ Var[f; Measure.map (⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm) (multivariateGaussian 0 (covMatrix I))] =
    Var[f ∘ ofLp; multivariateGaussian 0 (covMatrix I)]

Tactic:
variance_map_equiv

Goal state after:
I : Finset ℝ≥0
f : (↥I → ℝ) → ℝ
⊢ Var[f ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm; multivariateGaussian 0 (covMatrix I)] =
    Var[f ∘ ofLp; multivariateGaussian 0 (covMatrix 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
inst✝ : Add T
h : IsGaussianProcess X P
t₀ : T
⊢ IsGaussianProcess (fun t ω ↦ X (t₀ + t) ω - X t₀ ω) P

Tactic:
classical
  exact h.of_isGaussianProcess fun t ↦ ⟨{t₀, t₀ + t},
    { toFun x := x ⟨t₀ + t, by simp⟩ - x ⟨t₀, by simp⟩
      map_add' x y := by simp; abel
      map_smul' c x := by simp; module },
    by simp⟩

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

Goal state before:
pp: case refine_1
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)
⊢ HasGaussianLaw (fun ω i j ↦ X (↑i) (↑j) ω) P

Tactic:
let L : (I.sigma (fun i ↦ if hi : i ∈ I then J ⟨i, hi⟩ else ∅) → E) →L[ℝ] (i : I) → J i → E :=
      { toFun x i j := x ⟨⟨i, j⟩, by simp⟩
        map_add' x y := by ext; simp
        map_smul' c x := by ext; simp }

Goal state after:
case refine_1
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)
L : (↥(I.sigma fun i ↦ if hi : i ∈ I then J ⟨i, hi⟩ else ∅) → E) →L[ℝ] (i : ↥I) → ↥(J i) → E :=
  { toFun := fun x i j ↦ x ⟨⟨↑i, ↑j⟩, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ HasGaussianLaw (fun ω i j ↦ X (↑i) (↑j) ω) 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 : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (fun i ω j ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᵐ[κ a] X' i j
s : Finset S
f✝ : S → Set Ω
g : (i : S) → Set ((fun i ↦ (j : T i) → 𝓧 i j) i)
mg : ∀ i ∈ s, MeasurableSet (g i)
hg : ∀ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i = f✝ i
h3 : ⋂ i ∈ s, f✝ i = ⋂ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i
h3' : ∀ (a : α), ∏ i ∈ s, (κ a) (f✝ i) = ∏ i ∈ s, (κ a) ((fun i ω j ↦ X' i j ω) i ⁻¹' g i)
I : (i : S) → Set (T i)
u : (i : S) → Set ((a : ↑(I i)) → 𝓧 i ↑a)
hI : ∀ i ∈ s, (I i).Countable
hu : ∀ i ∈ s, g i = (I i).domRestrict ⁻¹' u i
f : (i : S) → (j : T i) → Ω → 𝓧 i j
i : S
hi : i ∈ s
⊢ (fun i ω j ↦ f i j ω) i ⁻¹' (I i).domRestrict ⁻¹' u i = (fun i ω j ↦ f i j ω) i ⁻¹' g i

Tactic:
rw [hu i hi]

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 : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (fun i ω j ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᵐ[κ a] X' i j
s : Finset S
f✝ : S → Set Ω
g : (i : S) → Set ((fun i ↦ (j : T i) → 𝓧 i j) i)
mg : ∀ i ∈ s, MeasurableSet (g i)
hg : ∀ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i = f✝ i
h3 : ⋂ i ∈ s, f✝ i = ⋂ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i
h3' : ∀ (a : α), ∏ i ∈ s, (κ a) (f✝ i) = ∏ i ∈ s, (κ a) ((fun i ω j ↦ X' i j ω) i ⁻¹' g i)
I : (i : S) → Set (T i)
u : (i : S) → Set ((a : ↑(I i)) → 𝓧 i ↑a)
hI : ∀ i ∈ s, (I i).Countable
hu : ∀ i ∈ s, g i = (I i).domRestrict ⁻¹' u i
h4 :
  ∀ (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
    ⋂ i ∈ s, (fun i ω j ↦ f i j ω) i ⁻¹' g i = ⋂ i ∈ s, (fun i ω j ↦ f i j ω) i ⁻¹' (I i).domRestrict ⁻¹' u i
a : α
f : (i : S) → (j : T i) → Ω → 𝓧 i j
i : S
hi : i ∈ s
⊢ (κ a) ((fun i ω j ↦ f i j ω) i ⁻¹' g i) = (κ a) ((fun i ω j ↦ f i j ω) i ⁻¹' (I i).domRestrict ⁻¹' u i)

Tactic:
rw [hu i hi]

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 μ
⊢ ∃ C, 0 < C ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ

Tactic:
by
  -- If there exists `a > 0` such that `2⁻¹ < μ {x | ‖x‖ ≤ a} < 1`, we can call the previous lemma.
  by_cases h_meas_Ioo : ∃ a, 0 < a ∧ 2⁻¹ < μ {x | ‖x‖ ≤ a} ∧ μ {x | ‖x‖ ≤ a} < 1
  · obtain ⟨a, ha_pos, ha_gt, ha_lt⟩ : ∃ a, 0 < a ∧ 2⁻¹ < μ {x | ‖x‖ ≤ a} ∧ μ {x | ‖x‖ ≤ a} < 1 :=
      h_meas_Ioo
    exact exists_integrable_exp_sq_of_map_rotation_eq_self' h_rot ha_pos ha_gt ha_lt
  -- Otherwise, we can find `b > 0` such that the ball of radius `b` has full measure
  obtain ⟨b, hb⟩ : ∃ b, μ {x | ‖x‖ ≤ b} = 1 := by
    by_contra h_ne
    push Not at h_meas_Ioo h_ne
    suffices μ .univ ≤ 2⁻¹ by simp at this
    have h_le a : μ {x | ‖x‖ ≤ a} ≤ 2⁻¹ := by
      have h_of_pos a' (ha : 0 < a') : μ {x | ‖x‖ ≤ a'} ≤ 2⁻¹ := by
        by_contra h_lt
        refine h_ne a' ?_
        exact le_antisymm prob_le_one (h_meas_Ioo a' ha (not_le.mp h_lt))
      rcases le_or_gt a 0 with ha | ha
      · calc μ {x | ‖x‖ ≤ a}
        _ ≤ μ {x | ‖x‖ ≤ 1} := measure_mono fun x hx ↦ hx.trans (ha.trans (by positivity))
        _ ≤ 2⁻¹ := h_of_pos _ (by positivity)
      · exact h_of_pos a ha
    have h_univ : (Set.univ : Set E) = ⋃ a : ℕ, {x | ‖x‖ ≤ a} := by
      ext x
      simp only [Set.mem_univ, Set.mem_iUnion, Set.mem_ofPred_eq, true_iff]
      exact exists_nat_ge _
    rw [h_univ, Monotone.measure_iUnion]
    · simp [h_le]
    · intro a b hab x hx
      simp only [Set.mem_ofPred_eq] at hx ⊢
      exact hx.trans (mod_cast hab)
  -- So we can take `C = 1` and show that `x ↦ exp (‖x‖ ^ 2)` is integrable, since it is bounded.
  have hb' : ∀ᵐ x ∂μ, ‖x‖ ≤ b := by
    rwa [ae_iff_prob_eq_one]
    refine measurable_to_prop ?_
    rw [show (fun x : E ↦ ‖x‖ ≤ b) ⁻¹' {True} = {x : E | ‖x‖ ≤ b} by ext; simp]
    exact measurableSet_le (by fun_prop) (by fun_prop)
  refine ⟨1, by positivity, ?_⟩
  refine integrable_of_le_of_le (g₁ := 0) (g₂ := fun _ ↦ rexp (b ^ 2)) (by fun_prop)
    ?_ ?_ (integrable_const _) (integrable_const _)
  · exact ae_of_all _ fun _ ↦ by positivity
  · filter_upwards [hb'] with x hx
    simp only [one_mul]
    gcongr

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

Goal state before:

Tactic:
(μ'.prod μ').map (ContinuousLinearMap.rotation (-(π / 4)))
    _ = ((μ Set.univ)⁻¹ * (μ Set.univ)⁻¹)
        • (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) := by
      simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul]
    _ = ((μ Set.univ)⁻¹ * (μ Set.univ)⁻¹) • (μ.prod μ) := by rw [h_rot]
    _ = μ'.prod μ' := by
      simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
r r' : ℚ
hrr' : r ≤ r'
⊢ ∀ᵐ (c : α) ∂(Kernel.const Unit ρ.fst) a, (preCDF ρ r (a, c).2).toReal ≤ (preCDF ρ r' (a, c).2).toReal

Tactic:
filter_upwards [monotone_preCDF ρ, preCDF_le_one ρ] with a h₁ h₂
    exact ENNReal.toReal_mono ((h₂ _).trans_lt ENNReal.one_lt_top).ne (h₁ hrr')

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Antitone s
hs_tendsto : Tendsto s atTop atBot
⊢ Tendsto (fun m ↦ ∫ (c : α), (preCDF ρ (s m) (a, c).2).toReal ∂(Kernel.const Unit ρ.fst) a) atTop (𝓝 0)

Tactic:
simp_rw [Kernel.const_apply, integral_preCDF_fst ρ]
    have h := ρ.tendsto_IicSnd_atBot MeasurableSet.univ
    rw [← ENNReal.toReal_zero]
    have h0 : Tendsto ENNReal.toReal (𝓝 0) (𝓝 0) :=
      ENNReal.continuousAt_toReal ENNReal.zero_ne_top
    exact h0.comp (h.comp hs_tendsto)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
⊢ IsMarkovKernel κ.condKernelReal

Tactic:
rw [condKernelReal]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
⊢ IsMarkovKernel (IsCondKernelCDF.toKernel κ.condKernelCDF ⋯)
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst✝² : Nonempty Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
⊢ (borelMarkovFromReal Ω η) a =
    if (η a) (range (embeddingReal Ω))ᶜ = 0 then Measure.comap (embeddingReal Ω) (η a)
    else Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose ⋯))

Tactic:
rw [borelMarkovFromReal, comapRight_apply, piecewise_apply, deterministic_apply]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst✝² : Nonempty Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
⊢ Measure.comap (embeddingReal Ω)
      (if a ∈ (fun a ↦ (η a) (range (embeddingReal Ω))ᶜ) ⁻¹' {0} then η a else Measure.dirac (Exists.choose ⋯)) =
    if (η a) (range (embeddingReal Ω))ᶜ = 0 then Measure.comap (embeddingReal Ω) (η a)
    else Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose ⋯))
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case h.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ MemLp (⇑L ∘ (Y - X)) 2 P

Tactic:
rw [map_comp_sub]
    exact (hY.map L).memLp_two.sub (hX.map L).memLp_two

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

Goal state before:
pp: β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f x ∂ρ

Tactic:
by
  rw [← setLIntegral_condKernel hf MeasurableSet.univ ht]; simp_rw [Measure.restrict_univ]

Goal state after: