gaussianPDFReal_mul — Mathlib

English

For μ ∈ ℝ, v ∈ ℝ≥0, c ∈ ℝ with c ≠ 0, and x ∈ ℝ, gaussianPDFReal μ v (c x) = |c⁻¹| gaussianPDFReal (c⁻¹ μ) (⟨(c²)⁻¹, inv_nonneg.mpr (sq_nonneg _)⟩ * v) x.

Русский

Для μ ∈ ℝ, v ∈ ℝ≥0, c ∈ ℝ, c ≠ 0, и x ∈ ℝ, gaussianPDFReal μ v (c x) = |c⁻¹| gaussianPDFReal (c⁻¹ μ) (⟨(c²)⁻¹, inv_nonneg.mpr (sq_nonneg _)⟩ * v) x.

LaTeX

$$$gaussianPDFReal\\mu \\ v (c \\ x) = |c^{-1}| \\ gaussianPDFReal (c^{-1} \\mu) (⟨(c^2)^{-1}, inv\\_nonneg.mpr (sq\\_nonneg _)\\rangle * v) x$$$

Lean4

theorem gaussianPDFReal_mul {μ : ℝ} {v : ℝ≥0} {c : ℝ} (hc : c ≠ 0) (x : ℝ) :
    gaussianPDFReal μ v (c * x) = |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (⟨(c ^ 2)⁻¹, inv_nonneg.mpr (sq_nonneg _)⟩ * v) x :=
  by
  conv_lhs => rw [← inv_inv c, gaussianPDFReal_inv_mul (inv_ne_zero hc)]
  simp

Похожие утверждения