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

Goal state before:
pp: case 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 μ
⊢ Integrable (fun ω ↦ X ω ^ p * rexp (v * X ω)) μ

pp: case refine_1
Ω : 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
⊢ v + t ≠ v - t

Tactic:
swap

Goal state after:
case refine_1
Ω : 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
⊢ v + t ≠ v - t

case 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 μ
⊢ Integrable (fun ω ↦ X ω ^ p * rexp (v * X ω)) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_1
Ω : 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
⊢ v + t - (v - t) ≠ 0

Tactic:
simp [ht]

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

Goal state before:
pp: Ω : 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:
simp [ht]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Tactic:
induction n generalizing z with
  | zero => simp [hasDerivAt_complexMGF hz]
  | succ n hn =>
    rw [iteratedDeriv_succ]
    have : deriv (iteratedDeriv n (complexMGF X μ))
        =ᶠ[𝓝 z] fun z ↦ μ[fun ω ↦ X ω ^ (n + 1) * cexp (z * X ω)] := by
      have h_mem : ∀ᶠ y in 𝓝 z, y.re ∈ interior (integrableExpSet X μ) := by
        refine IsOpen.eventually_mem ?_ hz
        exact isOpen_interior.preimage Complex.continuous_re
      filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
    rw [EventuallyEq.hasDerivAt_iff this]
    exact hasDerivAt_integral_pow_mul_exp hz (n + 1)

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 Ω'
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 μ')}
⊢ ↑t ∈ {z | z.re ∈ interior (integrableExpSet Y μ')}

Tactic:
simp [ht]

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

Goal state before:
pp: case neg
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal (∫ (x : ℝ) in s', |c⁻¹| * gaussianPDFReal μ v (e x)) =
    ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v) x)

pp: μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ NNReal.mk (c ^ 2) ⋯ * v ≠ 0

Tactic:
swap

Goal state after:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ NNReal.mk (c ^ 2) ⋯ * v ≠ 0

case neg
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal (∫ (x : ℝ) in s', |c⁻¹| * gaussianPDFReal μ v (e x)) =
    ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v) x)
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun a ↦ ‖↑(|X a| ^ p) * cexp (z * ↑(X a))‖) μ

pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun ω ↦ ↑(|X ω| ^ p) * cexp (z * ↑(X ω))) μ

Tactic:
swap

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun ω ↦ ↑(|X ω| ^ p) * cexp (z * ↑(X ω))) μ

Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun a ↦ ‖↑(|X a| ^ p) * cexp (z * ↑(X a))‖) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun a ↦ ‖↑(X a ^ p) * cexp (z * ↑(X a))‖) μ

pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun ω ↦ ↑(X ω ^ p) * cexp (z * ↑(X ω))) μ

Tactic:
swap

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun ω ↦ ↑(X ω ^ p) * cexp (z * ↑(X ω))) μ

Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun a ↦ ‖↑(X a ^ p) * cexp (z * ↑(X a))‖) μ
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case neg
μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x y : ℝ
h : ¬MemLp id 2 μ
⊢ ((covarianceBilin μ) x) y = x * y * Var[id; μ]

Tactic:
· simp [h, variance_of_not_memLp, aestronglyMeasurable_id]

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

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x : ℝ
⊢ ((covarianceBilin μ) x) x = x ^ 2 * Var[id; μ]

Tactic:
rw [covarianceBilin_real, pow_two]

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ charFun (Measure.map (⇑L) μ) 1 = charFun (gaussianReal (∫ (x : E), L x ∂μ) Var[⇑L; μ].toNNReal) 1

Tactic:
rw [IsGaussian.map_eq_gaussianReal L]

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

Goal state before:
pp: case e_a.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ ↑(∫ (x : E), L x ∂μ) = ∫ (x : E), ↑(L x) ∂μ

Tactic:
rw [integral_complex_ofReal]

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

Goal state before:
pp: case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
⊢ ‖(toLpₗ μ p) L‖ ≤ ‖L‖ * (eLpNorm id p μ).toReal

pp: case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : ¬MemLp id p μ
⊢ ‖(toLpₗ μ p) L‖ ≤ ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
swap

Goal state after:
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : ¬MemLp id p μ
⊢ ‖(toLpₗ μ p) L‖ ≤ ‖L‖ * (eLpNorm id p μ).toReal

case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
⊢ ‖(toLpₗ μ p) L‖ ≤ ‖L‖ * (eLpNorm id p μ).toReal
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case pos
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : CompleteSpace E
hμ : MemLp id 2 μ
⊢ (↑(covarianceOperator μ)).IsPositive

pp: case neg
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : CompleteSpace E
hμ : ¬MemLp id 2 μ
⊢ (↑(covarianceOperator μ)).IsPositive

Tactic:
swap

Goal state after:
case neg
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : CompleteSpace E
hμ : ¬MemLp id 2 μ
⊢ (↑(covarianceOperator μ)).IsPositive

case pos
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : CompleteSpace E
hμ : MemLp id 2 μ
⊢ (↑(covarianceOperator μ)).IsPositive
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ c + x) μ)

Tactic:
simp_rw [add_comm c]; infer_instance

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✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ (μ.prod μ) (⇑(ContinuousLinearMap.rotation (-(π / 4))) ⁻¹' {p | ‖p.1‖ ≤ a ∧ b < ‖p.2‖}) =
    (μ.prod μ) {p | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2}

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 : ℝ
⊢ MeasurableSet {p | ‖p.1‖ ≤ a ∧ b < ‖p.2‖}

Tactic:
swap

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✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ MeasurableSet {p | ‖p.1‖ ≤ a ∧ b < ‖p.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 : ℝ
⊢ (μ.prod μ) (⇑(ContinuousLinearMap.rotation (-(π / 4))) ⁻¹' {p | ‖p.1‖ ≤ a ∧ b < ‖p.2‖}) =
    (μ.prod μ) {p | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2}
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case h₁
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this : ∫⁻ (x : E), ‖L x‖ₑ ^ p.toReal ∂μ ≤ ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
h : (∫⁻ (x : E), ‖id x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≠ ∞
⊢ ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ ≠ ∞

Tactic:
simpa [h0] using h

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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
x : E
⊢ ‖L x‖ₑ ^ p.toReal ≤ (‖L‖ₑ * ‖x‖ₑ) ^ p.toReal

pp: case hz
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
x : E
⊢ 0 ≤ p.toReal

Tactic:
swap

Goal state after:
case hz
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
x : E
⊢ 0 ≤ p.toReal

E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
x : E
⊢ ‖L x‖ₑ ^ p.toReal ≤ (‖L‖ₑ * ‖x‖ₑ) ^ p.toReal
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: case e_a.e_a
E : Type u_1
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : BorelSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopologyEither E F
ν : Measure F
inst✝ : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inl ℝ E F
hL₁ : L₁ = L ∘SL ContinuousLinearMap.inl ℝ E F
L₂ : F →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inr ℝ E F
hL₂ : L₂ = L ∘SL ContinuousLinearMap.inr ℝ E F
⊢ ∫ (x : E), ↑(L₁ x) ∂μ + ∫ (x : F), ↑(L₂ x) ∂ν = ∫ (x : E × F), ↑(L x) ∂μ.prod ν

pp: case e_a
E : Type u_1
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : BorelSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopologyEither E F
ν : Measure F
inst✝ : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inl ℝ E F
hL₁ : L₁ = L ∘SL ContinuousLinearMap.inl ℝ E F
L₂ : F →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inr ℝ E F
hL₂ : L₂ = L ∘SL ContinuousLinearMap.inr ℝ E F
⊢ ↑Var[⇑L₁; μ] / 2 + ↑Var[⇑L₂; ν] / 2 = ↑Var[⇑L; μ.prod ν] / 2

Tactic:
· simp_rw [integral_complex_ofReal]
    rw [integral_continuousLinearMap_prod' (IsGaussian.integrable_dual μ (L.comp (.inl ℝ E F)))
      (IsGaussian.integrable_dual ν (L.comp (.inr ℝ E F)))]
    norm_cast

Goal state after:
case e_a
E : Type u_1
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : BorelSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopologyEither E F
ν : Measure F
inst✝ : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inl ℝ E F
hL₁ : L₁ = L ∘SL ContinuousLinearMap.inl ℝ E F
L₂ : F →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inr ℝ E F
hL₂ : L₂ = L ∘SL ContinuousLinearMap.inr ℝ E F
⊢ ↑Var[⇑L₁; μ] / 2 + ↑Var[⇑L₂; ν] / 2 = ↑Var[⇑L; μ.prod ν] / 2
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ ‖((uncenteredCovarianceBilinDual μ) L₁) L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), ‖x‖ ^ 2 ∂μ

pp: case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : ¬MemLp id 2 μ
⊢ ‖((uncenteredCovarianceBilinDual μ) L₁) L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), ‖x‖ ^ 2 ∂μ

Tactic:
swap

Goal state after:
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : ¬MemLp id 2 μ
⊢ ‖((uncenteredCovarianceBilinDual μ) L₁) L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), ‖x‖ ^ 2 ∂μ

case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ ‖((uncenteredCovarianceBilinDual μ) L₁) L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), ‖x‖ ^ 2 ∂μ
Module: Mathlib.Probability.Moments.CovarianceBilinDual

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

Tactic:
simp [h]

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h' : IsGaussian μ
n : StrongDual ℝ E → ℤ
hn :
  ∀ (L : StrongDual ℝ E),
    ↑(L (∫ (x : E), id x ∂μ)) * I - ↑(((covarianceBilinDual μ) L) L) / 2 =
      ↑(L m) * I - ↑((f L) L) / 2 + ↑(n L) * (2 * ↑π * I)
h :
  ∀ (L : StrongDual ℝ E),
    ↑(n L) =
      (↑(L (∫ (x : E), id x ∂μ)) * I - ↑(((covarianceBilinDual μ) L) L) / 2 - ↑(L m) * I + ↑((f L) L) / 2) /
        (2 * ↑π * I)
this✝ : Continuous n
this : ∀ (x : StrongDual ℝ E), n = Function.const (StrongDual ℝ E) (n x)
L : StrongDual ℝ E
⊢ ↑(Function.const (StrongDual ℝ E) (n 0) L) = ↑0

Tactic:
simp [h]

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

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : CompleteSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : NormedSpace ℝ E
ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
h : μ = ν
⊢ ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν ∧ covarianceBilinDual μ = covarianceBilinDual ν

Tactic:
simp [h]

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
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
⊢ μ {x} = 0

Tactic:
obtain ⟨L, hL⟩ : ∃ L : StrongDual ℝ E, Var[L; μ] ≠ 0 := by
      contrapose! h
      exact ⟨_, eq_dirac_of_variance_eq_zero h⟩
    have hL_zero : μ.map L {L x} = 0 := by
      have : NullSingletonClass (μ.map L) := by
        rw [map_eq_gaussianReal L]
        refine nullSingletonClass_gaussianReal ?_
        simp only [ne_eq, Real.toNNReal_eq_zero, not_le]
        exact lt_of_le_of_ne (variance_nonneg _ _) hL.symm
      rw [measure_singleton]
    rw [Measure.map_apply (by fun_prop) (measurableSet_singleton _)] at hL_zero
    refine measure_mono_null ?_ hL_zero
    exact fun ⦃a⦄ ↦ congrArg ⇑L

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

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : CompleteSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : InnerProductSpace ℝ E
ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
h : μ = ν
⊢ ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν ∧ covarianceBilin μ = covarianceBilin ν

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ ↑(hf.stieltjesFunction a) x ≤ 1

Tactic:
obtain ⟨r, hrx⟩ := exists_rat_gt x

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
⊢ ↑(hf.stieltjesFunction a) x ≤ 1
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
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
⊢ Nonempty { r' // x < ↑r' }

Tactic:
obtain ⟨r, hrx⟩ := exists_rat_gt x

Goal state after:
α : 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
r : ℚ
hrx : x < ↑r
⊢ Nonempty { r' // x < ↑r' }
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: case hfm
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ AEMeasurable (preCDF ρ r) (ρ.fst.restrict s)

pp: case hf
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ ∀ᵐ (x : α) ∂ρ.fst.restrict s, preCDF ρ r x < ∞

Tactic:
· exact measurable_preCDF.aemeasurable

Goal state after:
case hf
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ ∀ᵐ (x : α) ∂ρ.fst.restrict s, preCDF ρ r x < ∞
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
s t : ℝ≥0
hst : s ≤ t
⊢ cov[fun ω ↦ (√↑c)⁻¹ * B (c * s) ω, fun ω ↦ (√↑c)⁻¹ * B (c * t) ω; P] = ↑s

Tactic:
rw [covariance_const_mul_left, covariance_const_mul_right, hB.covariance_eval, min_eq_left]

Goal state after:
case refine_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
s t : ℝ≥0
hst : s ≤ t
⊢ (√↑c)⁻¹ * ((√↑c)⁻¹ * ↑(c * s)) = ↑s

case refine_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
s t : ℝ≥0
hst : s ≤ t
⊢ c * s ≤ c * t