ASTIS mathematical exposition

The scalar square-root/logarithm coefficients give a factor of one quarter

AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainScalar · theorem · Teaching coverage

Statement

For any positive real r and any real dr, the squared expression dr/(2√r) equals one quarter of r times (dr/r)². The symbols are numbers, not derivatives whose existence is established here.

\[r>0\Longrightarrow\left(\frac{dr}{2\sqrt r}\right)^2=\frac14\,r\left(\frac{dr}{r}\right)^2.\]

All objects and hypotheses

r,dr∈ℝ; hr asserts r>0. Strict positivity, not mere nonnegativity, permits clearing both denominators.

Mathematical proof

1. Record the square-root and nonzero facts

Positivity gives (√r)²=r and both r≠0 and √r≠0.

\[(\sqrt r)^2=r,\qquad r\ne0,\qquad\sqrt r\ne0.\]

Corresponding Lean step

Real.sq_sqrt; Real.sqrt_pos; hsqrt_sq, hsqrt_ne, hr_ne

2. Clear the nonzero denominators

Cross-multiplication reduces the rational equality to polynomial arithmetic; the two sides agree after replacing (√r)² by r.

\[\frac{dr^2}{4(\sqrt r)^2}=\frac{dr^2}{4r}=\frac14\,r\,\frac{dr^2}{r^2}.\]

Corresponding Lean step

field_simp [hsqrt_ne,hr_ne]; nlinarith [hsqrt_sq]

Lean statement · lsiKlFiSqrtDensityFisherChainScalar

dr is any real number. The theorem identifies a coefficient pattern used by a future derivative calculation, not a derivative of a function.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem lsiKlFiSqrtDensityFisherChainScalar {r dr : Real} (hr : 0 < r) :
    ((1 / (2 * Real.sqrt r)) * dr) ^ 2 =
      (1 / 4) * (r * (dr / r) ^ 2)

Exact module and namespace context

Lean proof · lsiKlFiSqrtDensityFisherChainScalar

The proof first establishes that the denominators are nonzero, then reduces the equation to polynomial arithmetic with the square-root identity.

theorem lsiKlFiSqrtDensityFisherChainScalar {r dr : Real} (hr : 0 < r) :
    ((1 / (2 * Real.sqrt r)) * dr) ^ 2 =
      (1 / 4) * (r * (dr / r) ^ 2) := by
  have hsqrt_sq : (Real.sqrt r) ^ 2 = r := Real.sq_sqrt (le_of_lt hr)
  have hsqrt_ne : Real.sqrt r ≠ 0 := ne_of_gt (Real.sqrt_pos.2 hr)
  have hr_ne : r ≠ 0 := ne_of_gt hr
  field_simp [hsqrt_ne, hr_ne]
  nlinarith [hsqrt_sq]

/-- Pointwise Fisher-chain handoff with named derivative identities.

This packages the scalar part of
`nabla sqrt(r) = (2*sqrt(r))^{-1} nabla r` and
`nabla log r = r^{-1} nabla r`.  It does not prove differentiability,
gradient existence, or the vector norm/integral transport backend.
-/

Exact module and namespace context

Scope and omitted-condition boundaries

These are scalar, density-integral or supplied-derivative handoffs. They do not prove an LSI, the admissibility of its square-root-density test, the vector/Sobolev chain rule or the full KL–Fisher comparison.
The r=0 case is excluded; no zero-density extension or vector-norm identity is proved.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

Real.sq_sqrt
Real.sqrt_pos

Mathematical sources

Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
Real.sq_sqrt — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.
Real.sqrt_pos — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.