mathlib-initiative/mathlib-tactics huggingface dataset:
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
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
u v : StrongDual 𝕜 E
⊢ MemLp.toLp ⇑(u + v) ⋯ = MemLp.toLp ⇑u ⋯ + MemLp.toLp ⇑v ⋯

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
⊢ AEMeasurable (fun x ↦ c + x) μ

Tactic:
by

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
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ MemLp.toLp (c • ⇑L) ⋯ = id c • MemLp.toLp ⇑L ⋯

Tactic:
MemLp.toLp_const_smul

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ c • MemLp.toLp ⇑L ?hf = id c • MemLp.toLp ⇑L ⋯

case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ MemLp (⇑L) p μ
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
⊢ AEStronglyMeasurable
    (fun z ↦
      ⟪x, z - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫ * ⟪y, z - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫)
    (Measure.map (fun x ↦ c + x) μ)

Tactic:
by

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
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ MemLp.toLp ⇑(c • L) ⋯ = (RingHom.id 𝕜) c • MemLp.toLp ⇑L ⋯

Tactic:
by

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
h_Lp : MemLp id p μ
L : StrongDual 𝕜 E
⊢ (toLpₗ μ p) L = MemLp.toLp ⇑L ⋯

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
z : E
⊢ AEMeasurable (fun x ↦ c + x) μ

Tactic:
by

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
h_Lp : ¬MemLp id p μ
L : StrongDual 𝕜 E
⊢ (toLpₗ μ p) L = 0

Tactic:
by

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✝ : IsFiniteMeasure μ
⊢ IsGaussian μ ↔ ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)

Tactic:
by

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

Goal state before:
pp: E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
t : E
⊢ charFun μ t = cexp ((∫ (x : E), ↑((fun x ↦ ⟪t, x⟫) x) ∂μ) * I - ↑Var[fun x ↦ ⟪t, x⟫; μ] / 2)

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
z : E
⊢ 1 ≤ 2

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ Measure.map (X + Y) P = gaussianReal (m₁ + m₂) (v₁ + v₂)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ Measure.map (X + Y) P = gaussianReal (m₁ + m₂) (v₁ + v₂)

Tactic:
by
  rw [hXY.map_add_eq_map_conv_map₀', hX, hY, gaussianReal_conv_gaussianReal]
  · apply AEMeasurable.of_map_ne_zero; simp [NeZero.ne, hX]
  · apply AEMeasurable.of_map_ne_zero; simp [NeZero.ne, hY]
  · rw [hX]; apply IsFiniteMeasure.toSigmaFinite
  · rw [hY]; apply IsFiniteMeasure.toSigmaFinite

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
⊢ covarianceBilin (Measure.map (fun x ↦ c + x) μ) = covarianceBilin μ

Tactic:
by

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

Goal state before:
pp: E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
⊢ IsGaussian μ ↔ ∀ (t : E), charFun μ t = cexp ((∫ (x : E), ↑((fun x ↦ ⟪t, x⟫) x) ∂μ) * I - ↑Var[fun x ↦ ⟪t, x⟫; μ] / 2)

Tactic:
by

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
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
this : (essSup (fun x ↦ ‖L x‖ₑ) μ).toReal ≤ (essSup (fun x ↦ ‖L‖ₑ * ‖x‖ₑ) μ).toReal
⊢ (essSup (fun x ↦ ‖L x‖ₑ) μ).toReal ≤ ‖L‖ * (essSup (fun x ↦ ‖x‖ₑ) μ).toReal

Tactic:
by

Goal state after:
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 μ✝
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
L : StrongDual ℝ E
⊢ AEMeasurable (⇑L) (μ ∗ ν)

Tactic:
by

Goal state after:
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 μ✝
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
L : StrongDual ℝ E
⊢ AEStronglyMeasurable (fun x ↦ x) (Measure.map (⇑L) (μ ∗ ν))

Tactic:
by

Goal state after:
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 μ✝
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
L : StrongDual ℝ E
⊢ ∫ (x : E), L x ∂μ ∗ ν = ∫ (x : ℝ), x ∂Measure.map (⇑L) μ ∗ Measure.map (⇑L) ν

Tactic:
by

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
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
⊢ ‖L‖ₑ ≠ ∞

Tactic:
by

Goal state after:
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 μ✝
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
L : StrongDual ℝ E
this : ∫ (x : E), L x ∂μ ∗ ν = ∫ (x : ℝ), x ∂Measure.map (⇑L) μ ∗ Measure.map (⇑L) ν
⊢ AEMeasurable (⇑L) (μ ∗ ν)

Tactic:
by

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 = ∞
⊢ 0 < p.toReal

Tactic:
by

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) μ
⊢ Measurable fun u ↦ ⟪(basisFun ι ℝ) i, u⟫

Tactic:
by

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) μ
⊢ Measurable fun u ↦ ⟪(basisFun ι ℝ) j, u⟫

Tactic:
by

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
this : ‖(toLpₗ μ p) L‖ ≤ (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ 0 ≤ ‖L‖ₑ.toReal ^ p.toReal

Tactic:
by

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
this : ‖(toLpₗ μ p) L‖ ≤ (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ 0 ≤ (∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal

Tactic:
by

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) μ
⊢ AEMeasurable (fun ω ↦ toLp 2 fun x ↦ X x ω) μ

Tactic:
by

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 : ι
⊢ ((covarianceBilin (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)) ((basisFun ι ℝ) i)) ((basisFun ι ℝ) j) =
    cov[X i, X j; μ]

Tactic:
by

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
this : ‖(toLpₗ μ p) L‖ ≤ (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ 0 ≤ ‖L‖ₑ.toReal

Tactic:
by

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 : ι
⊢ ((covarianceBilin (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)) ((basisFun ι ℝ) i)) ((basisFun ι ℝ) i) = Var[X i; μ]

Tactic:
by

Goal state after:
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 μ✝
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
L : StrongDual ℝ E
⊢ Measure.map (⇑L) (μ ∗ ν) = gaussianReal (∫ (x : E), L x ∂μ ∗ ν) Var[⇑L; μ ∗ ν].toNNReal

Tactic:
by

Goal state after:
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
L : StrongDual ℝ E
⊢ (⇑L ∘ fun x ↦ x + c) = fun x ↦ L x + L c

Tactic:
by

Goal state after:
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
L : StrongDual ℝ E
hL_comp : (⇑L ∘ fun x ↦ x + c) = fun x ↦ L x + L c
⊢ AEMeasurable (⇑L) (Measure.map (fun x ↦ x + c) μ)

Tactic:
by

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
this : ‖(toLpₗ μ p) L‖ ≤ (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ p ≠ 0

Tactic:
by

Goal state after:
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
L : StrongDual ℝ E
hL_comp : (⇑L ∘ fun x ↦ x + c) = fun x ↦ L x + L c
⊢ AEMeasurable (fun x ↦ x + c) μ

Tactic:
by

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

Goal state before:
pp: β : Type u_1
inst✝ : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
ht_tendsto : Tendsto t atTop atTop
x : β
hx : t 0 < x
⊢ ∃ n, x ≤ t n

Tactic:
by

Goal state after:
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
L : StrongDual ℝ E
hL_comp : (⇑L ∘ fun x ↦ x + c) = fun x ↦ L x + L c
⊢ AEStronglyMeasurable (fun x ↦ ↑(L x)) (Measure.map (fun x ↦ x + c) μ)

Tactic:
by

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

Goal state before:
pp: β : Type u_1
inst✝ : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
ht_tendsto : Tendsto t atTop atTop
x : β
hx : t 0 < x
h : ∃ n, x ≤ t n
h' : ∀ m < Nat.find h, t m < x
⊢ Nat.find h - 1 < Nat.find h

Tactic:
by

Goal state after:
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
L : StrongDual ℝ E
hL_comp : (⇑L ∘ fun x ↦ x + c) = fun x ↦ L x + L c
⊢ AEStronglyMeasurable (⇑L) μ

Tactic:
by

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

Goal state before:
pp: β : Type u_1
inst✝ : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
ht_tendsto : Tendsto t atTop atTop
x : β
hx : t 0 < x
h : ∃ n, x ≤ t n
h' : ∀ m < Nat.find h, t m < x
⊢ x ≤ t (Nat.find h - 1 + 1)

Tactic:
by

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
this : ‖(toLpₗ μ p) L‖ ≤ (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ ‖(toLpₗ μ p) L‖ ≤ ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
by

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

Goal state before:
pp: β : Type u_1
inst✝ : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
ht_tendsto : Tendsto t atTop atTop
x : β
hx : t 0 < x
⊢ ∃ n, t n < x ∧ x ≤ t (n + 1)

Tactic:
by

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) μ
⊢ Measurable fun u ↦ ⟪x, u⟫

Tactic:
by

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) μ
⊢ Measurable fun u ↦ ⟪y, u⟫

Tactic:
by

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) μ
⊢ Measurable ?m.351

Tactic:
by

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) μ
⊢ Measurable ?m.351
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
⊢ p ≠ 0

Tactic:
by

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) μ
⊢ AEMeasurable (fun ω ↦ toLp 2 fun x ↦ X x ω) μ

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
θ : ℝ
x y : E × E
⊢ (Real.cos θ • (x + y).1 + Real.sin θ • (x + y).2, -Real.sin θ • (x + y).1 + Real.cos θ • (x + y).2) =
    (Real.cos θ • x.1 + Real.sin θ • x.2, -Real.sin θ • x.1 + Real.cos θ • x.2) +
      (Real.cos θ • y.1 + Real.sin θ • y.2, -Real.sin θ • y.1 + Real.cos θ • y.2)

Tactic:
by

Goal state after:
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
L : StrongDual ℝ E
hL_comp : (⇑L ∘ fun x ↦ x + c) = fun x ↦ L x + L c
⊢ Integrable (⇑L) μ

Tactic:
by

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 ℝ ι
⊢ ((covarianceBilin (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)) x) y =
    ∑ i, ∑ j, x.ofLp i * y.ofLp j * cov[X i, X j; μ]

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace E
⊢ covarianceOperator 0 = 0

Tactic:
by

Goal state after:
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
L : StrongDual ℝ E
hL_comp : (⇑L ∘ fun x ↦ x + c) = fun x ↦ L x + L c
⊢ Integrable (fun x ↦ L c) μ

Tactic:
by

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

Goal state before:
pp: 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 μ = 0

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
θ c : ℝ
x : E × E
⊢ (Real.cos θ • (c • x).1 + Real.sin θ • (c • x).2, -Real.sin θ • (c • x).1 + Real.cos θ • (c • x).2) =
    (RingHom.id ℝ) c • (Real.cos θ • x.1 + Real.sin θ • x.2, -Real.sin θ • x.1 + Real.cos θ • x.2)

Tactic:
by

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

Goal state before:
pp: 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 μ
x y : E
⊢ ⟪(covarianceOperator μ) x, y⟫ = ∫ (z : E), ⟪x, z⟫ * ⟪y, z⟫ ∂μ

Tactic:
by

Goal state after: