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

Goal state before:
pp: case hc
Ω : 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 ∂μ
⊢ DifferentiableAt ℝ (deriv (mgf X μ)) v

Tactic:
← iteratedDeriv_one

Goal state after:
case hc
Ω : 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 ∂μ
⊢ DifferentiableAt ℝ (iteratedDeriv 1 (mgf X μ)) v
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ (ℙ.withDensity (gaussianPDF μ v)) s = ∫⁻ (x : ℝ) in s, gaussianPDF μ v x

Tactic:
withDensity_apply' _ s

Goal state after:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ ∫⁻ (a : ℝ) in s, gaussianPDF μ v a = ∫⁻ (x : ℝ) in s, gaussianPDF μ v x
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
⊢ ∂ℙ.withDensity (gaussianPDF μ v)/∂ℙ =ᵐ[ℙ] gaussianPDF μ v

Tactic:
exact Measure.rnDeriv_withDensity _ (measurable_gaussianPDF μ v)

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

Goal state before:
pp: Ω : 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 ω)) μ
n : ℕ
⊢ Integrable (fun ω ↦ X ω ^ n) μ

Tactic:
convert!
    integrable_rpow_of_integrable_exp_mul ht ht_int_pos ht_int_neg
      (by positivity : 0 ≤ (n : ℝ)) with
    ω

Goal state after:
Ω : 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 ω)) μ
n : ℕ
ω : Ω
⊢ X ω ^ n = X ω ^ ↑n
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:
sub_eq_add_neg,

Goal state after:
μ : ℝ
v : ℝ≥0
y : ℝ
⊢ Measure.map (fun x ↦ x + -y) (gaussianReal μ v) = gaussianReal (μ + -y) v
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 : ∀ (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 μ'

Tactic:
specialize h (Multiplicative.toAdd w * I)

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 μ'
inner_ne_zero : ∀ (x : ℝ), x ≠ 0 → (innerₗ ℝ) x ≠ 0
w : ℝ
h : complexMGF X μ (↑(Multiplicative.toAdd w) * I) = complexMGF Y μ' (↑(Multiplicative.toAdd w) * I)
⊢ ∫ (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
⊢ Var[fun x ↦ x; gaussianReal μ v] = ↑v

Tactic:
variance_eq_integral measurable_id'.aemeasurable

Goal state after:
μ : ℝ
v : ℝ≥0
⊢ ∫ (ω : ℝ), (ω - ∫ (x : ℝ), x ∂gaussianReal μ v) ^ 2 ∂gaussianReal μ v = ↑v
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ ∫ (x : ℝ), L x ∂gaussianReal μ v = ∫ (x : ℝ), x ∂Measure.map (⇑L) (gaussianReal μ v)

Tactic:
rw [integral_map (φ := L) (by fun_prop) (by fun_prop)]

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

Goal state before:
pp: case neg.inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (fun x ↦ x - c) p μ
this : id = fun x ↦ x - c + c
hx : ¬c = 0
hp0 : p ≠ 0
hptop : p ≠ ∞
⊢ MemLp (fun x ↦ c) p μ

Tactic:
apply (integrable_norm_rpow_iff (by fun_prop) hp0 hptop).1

Goal state after:
case neg.inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ⋯
h_Lp : MemLp (fun x ↦ x - c) p μ
this : id = fun x ↦ x - c + c
hx : ¬c = 0
hp0 : p ≠ 0
hptop : p ≠ ∞
⊢ Integrable (fun x ↦ ‖c‖ ^ p.toReal) μ
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
h : ¬MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ((covarianceBilinDual μ) L₁) L₂ = 0

Tactic:
by
  apply covarianceBilinDual_of_not_memLp'
  contrapose h
  exact memLp_id_of_self_sub_integral h

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

Goal state before:
pp: case e_a
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ n = ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ n

pp: case e_a
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ (1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a} ≠ ∞

Tactic:
· norm_cast

Goal state after:
case e_a
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ (1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a} ≠ ∞
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
⊢ ‖x - y + y‖ ^ 2 ≤ (‖x - y‖ + ‖y‖) ^ 2

Tactic:
by grw [norm_add_le (x - y) y]

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
t : E
⊢ cexp (-(↑(‖t‖ ^ 2) / 2)) = cexp (-↑(‖t‖ ^ 2) / 2)

Tactic:
neg_div

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ ∫ (x : EuclideanSpace ℝ ι), x ∂multivariateGaussian μ S = μ

Tactic:
rw [multivariateGaussian, integral_map (by fun_prop) (by fun_prop),
    integral_add (integrable_const _), integral_const]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ (stdGaussian (EuclideanSpace ℝ ι)).real Set.univ • μ +
      ∫ (a : EuclideanSpace ℝ ι), (toEuclideanCLM (CFC.sqrt S)) a ∂stdGaussian (EuclideanSpace ℝ ι) =
    μ

ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ Integrable (⇑(toEuclideanCLM (CFC.sqrt S))) (stdGaussian (EuclideanSpace ℝ ι))
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case hab
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_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := ⋯
c : ℝ≥0∞ := ⋯
C : ℝ := ⋯
hc'_le : c' ≤ 1
x : E
hx : x ∈ closedBall 0 a
⊢ ‖x‖ ≤ a

Tactic:
simpa using hx

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

Goal state before:
pp: case hm
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ (EuclideanSpace.restrict₂ hJI) (∫ (x : EuclideanSpace ℝ ↥I), x ∂multivariateGaussian μ S) =
    (EuclideanSpace.restrict₂ hJI) μ

pp: case hm.h
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ Integrable id (multivariateGaussian μ S)

Tactic:
integral_id_multivariateGaussian

Goal state after:
case hm
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ (EuclideanSpace.restrict₂ hJI) μ = (EuclideanSpace.restrict₂ hJI) μ

case hm.h
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ Integrable id (multivariateGaussian μ S)
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
hX : HasIndepIncrements X P
t : ℕ → T
ht : Monotone t
⊢ iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P

Tactic:
by
  refine iIndepFun_iff_finset.2 fun s ↦ ?_
  obtain rfl | hs := s.eq_empty_or_nonempty
  · have := (hX 0 (fun _ ↦ t 0) (fun _ ↦ by grind)).isProbabilityMeasure
    exact iIndepFun.of_subsingleton
  · let g (x : s) : Fin (s.max' hs + 1) := ⟨x.1, Nat.lt_add_one_of_le (s.le_max' x.1 x.2)⟩
    refine iIndepFun.precomp (g := g) ?_ (hX (s.max' hs + 1) (fun m ↦ t m) ?_)
    · simp [g, Function.Injective]
    · exact ht.comp Fin.val_strictMono.monotone

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: ι : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : Fintype ι
inst✝¹ : NormedSpace ℝ E
μ : ι → Measure E
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
x✝ : i ∈ univ
⊢ charFunDual (Measure.map (fun p ↦ p i) (Measure.pi μ)) = charFunDual (μ i)

Tactic:
rw [(measurePreserving_eval μ i).map_eq]

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

Goal state before:
pp: S : Type u_1
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
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : S → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL : ∀ (s : S) (ω : Ω), Y s ω = (L s) ((J s).restrict fun x ↦ X x ω)
⊢ HasGaussianLaw (fun ω ↦ I.restrict fun x ↦ Y x ω) P

Tactic:
classical
    let K : (I.biUnion J → E) →L[ℝ] I → F :=
      { toFun x s := L s (fun t ↦ x ⟨t.1, mem_biUnion.2 ⟨s.1, s.2, t.2⟩⟩)
        map_add' x y := by ext; simp [← Pi.add_def]
        map_smul' c x := by ext; simp [← Pi.smul_def] }
    have : (fun ω ↦ I.restrict (Y · ω)) = K ∘ (fun ω ↦ (I.biUnion J).restrict (X · ω)) := by
      ext; simp [K, hL, Finset.restrict_def]
    rw [this]
    exact (hX.hasGaussianLaw _).map _

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 α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝¹ : (i : S) → MeasurableSpace (𝓧 i)
inst✝ : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (fun ω i ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᵐ[κ a] X' i
t : Set 𝓨
ht : MeasurableSet t
I : Set S
u : Set ((i : ↑I) → 𝓧 ↑i)
hI : I.Countable
hs : MeasurableSet (I.domRestrict ⁻¹' u)
this :
  ∀ᵐ (a : α) ∂P, (κ a) ((fun ω i ↦ X (↑i) ω) ⁻¹' u ∩ Y ⁻¹' t) = (κ a) ((fun ω i ↦ X (↑i) ω) ⁻¹' u) * (κ a) (Y ⁻¹' t)
aux : ∀ (f : (i : S) → Ω → 𝓧 i), True
x✝ : Countable ↑I
a : α
⊢ (∀ (i : ↑I), X ↑i =ᵐ[κ a] X' ↑i) → (fun ω i ↦ X (↑i) ω) =ᵐ[κ a] fun ω i ↦ X' (↑i) ω

Tactic:
(ha : ∀ (i : I), ∀ᵐ ω ∂κ a, X i ω = X' i ω)

Goal state after:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝¹ : (i : S) → MeasurableSpace (𝓧 i)
inst✝ : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (fun ω i ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᵐ[κ a] X' i
t : Set 𝓨
ht : MeasurableSet t
I : Set S
u : Set ((i : ↑I) → 𝓧 ↑i)
hI : I.Countable
hs : MeasurableSet (I.domRestrict ⁻¹' u)
this :
  ∀ᵐ (a : α) ∂P, (κ a) ((fun ω i ↦ X (↑i) ω) ⁻¹' u ∩ Y ⁻¹' t) = (κ a) ((fun ω i ↦ X (↑i) ω) ⁻¹' u) * (κ a) (Y ⁻¹' t)
aux : ∀ (f : (i : S) → Ω → 𝓧 i), True
x✝ : Countable ↑I
a : α
ha : ∀ (i : ↑I), ∀ᵐ (ω : Ω) ∂κ a, X (↑i) ω = X' (↑i) ω
⊢ (fun ω i ↦ X (↑i) ω) =ᵐ[κ a] fun ω i ↦ X' (↑i) ω
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 μ
a : ℝ
ha_pos : 0 < a
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
h_one_sub_lt_self : 1 - c < c
h_pos : 0 < logRatio c * a⁻¹ ^ 2
⊢ 1 < (c / (1 - c)).toReal

Tactic:
simp only [ENNReal.toReal_div, one_lt_div_iff, ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hc_lt,
    hc_one_sub_lt_top, and_self, true_and]

Goal state after:
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 μ
a : ℝ
ha_pos : 0 < a
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
h_one_sub_lt_self : 1 - c < c
h_pos : 0 < logRatio c * a⁻¹ ^ 2
⊢ (1 - c).toReal < c.toReal ∨ (1 - c).toReal < 0 ∧ c.toReal < (1 - c).toReal
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case neg.refine_2
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
hb' : ∀ᵐ (x : E) ∂μ, ‖x‖ ≤ b
⊢ (fun x ↦ rexp (1 * ‖x‖ ^ 2)) ≤ᵐ[μ] fun x ↦ rexp (b ^ 2)

Tactic:
filter_upwards [hb'] with x hx
    simp only [one_mul]
    gcongr

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

Goal state before:
pp: case hv
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
⊢ ∑ i, ∑ j, x.ofLp i * x.ofLp j * cov[fun ω ↦ ω i, fun ω ↦ ω j; Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P] =
    ((covarianceBilin (Measure.map (WithLp.toLp 2) (projectiveFamily I))) x) x

pp: case hv.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
⊢ ∀ (i : ↥I), MemLp (fun ω ↦ ω i) 2 (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)

Tactic:
covarianceBilin_apply_pi

Goal state after:
case hv
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
⊢ ∑ i, ∑ j, x.ofLp i * x.ofLp j * cov[fun ω ↦ ω i, fun ω ↦ ω j; Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P] =
    ∑ i, ∑ j, x.ofLp i * x.ofLp j * cov[fun ω ↦ ω i, fun ω ↦ ω j; projectiveFamily I]

case hv.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
⊢ ∀ (i : ↥I), MemLp (fun ω ↦ ω i) 2 (projectiveFamily I)

case hv.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
⊢ ∀ (i : ↥I), MemLp (fun ω ↦ ω i) 2 (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x ↦ ⋯.choose
⊢ Tendsto qs atTop atTop

Tactic:
tendsto_atTop_atTop

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x ↦ ⋯.choose
⊢ ∀ (b : ℚ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ qs a
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r r' : ℝ
h_le : r ≤ r'
⊢ ρ.IicSnd r ≤ ρ.IicSnd r'

Tactic:
by
  unfold IicSnd; gcongr

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)
⊢ (κ a) (s ×ˢ univ) - (κ a) (s ×ˢ t) = (κ a) (s ×ˢ tᶜ)

Tactic:
by
        rw [← measure_sdiff _ (hs.prod ht).nullMeasurableSet (measure_ne_top _ _)]
        · rw [prod_sdiff_prod, compl_eq_univ_sdiff]
          simp only [sdiff_self, empty_prod, union_empty]
        · rw [prod_subset_prod_iff]
          exact Or.inl ⟨subset_rfl, subset_univ t⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ eLpNorm (fun x ↦ κ.densityProcess ν n a x s) 1 (ν a) < ∞

Tactic:
exact (eLpNorm_densityProcess_le hκν n a s).trans_lt (measure_lt_top _ _)

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

Goal state before:
pp: case refine_2
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun n ↦ Iic ↑(s n)
x : ℝ
⊢ ∃ i, x ∈ s' i

Tactic:
tendsto_atTop_atTop

Goal state after:
case refine_2
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : ∀ (b : ℚ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ s a
s' : ℕ → Set ℝ := fun n ↦ Iic ↑(s n)
x : ℝ
⊢ ∃ i, x ∈ s' i
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✝ : IsMarkovKernel η
a : α
⊢ ((piecewise ⋯ η (deterministic (fun x ↦ Exists.choose ⋯) ⋯)) a) (range (embeddingReal Ω)) = 1

Tactic:
rw [piecewise_apply]
  split_ifs with h
  · rwa [← prob_compl_eq_zero_iff (measurableEmbedding_embeddingReal Ω).measurableSet_range]
  · rw [deterministic_apply]
    simp [(range_nonempty (embeddingReal Ω)).choose_spec]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
⊢ ∀ᵐ (t : β) ∂κ.fst a, (a, t) ∈ {p | (η p) (range e)ᶜ = 0}

Tactic:
rw [← h_fst]

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
⊢ ∀ᵐ (t : β) ∂κ'.fst a, (a, t) ∈ {p | (η p) (range e)ᶜ = 0}