gaussianPDFReal_inv_mul — Mathlib

English

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

Русский

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

LaTeX

$$$gaussianPDFReal\\mu \\ v (c^{-1} x) = |c| \\ gaussianPDFReal (c \\mu) (⟨c^2, sq\\_nonneg ⟩ * v) x$$$

Lean4

theorem gaussianPDFReal_inv_mul {μ : ℝ} {v : ℝ≥0} {c : ℝ} (hc : c ≠ 0) (x : ℝ) :
    gaussianPDFReal μ v (c⁻¹ * x) = |c| * gaussianPDFReal (c * μ) (⟨c ^ 2, sq_nonneg _⟩ * v) x :=
  by
  simp only [gaussianPDFReal.eq_1, NNReal.zero_le_coe, Real.sqrt_mul', mul_inv_rev, NNReal.coe_mul, NNReal.coe_mk]
  rw [← mul_assoc]
  refine congr_arg₂ _ ?_ ?_
  · simp (disch := positivity) only [Real.sqrt_mul, mul_inv_rev, field]
    rw [Real.sqrt_sq_eq_abs]
  · congr 1
    field_simp

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