logRatio — Mathlib

English

The quantity logRatio is defined by logRatio(c) = log(c/(1−c)) / (8(1+√2)^2).

Русский

Показатель logRatio определяется как logRatio(c) = log(c/(1−c)) / (8(1+√2)^2).

LaTeX

$$\\operatorname{logRatio}(c) = \\dfrac{\\log\\left( \\dfrac{c}{1-c} \\right)}{8\\,(1+\\sqrt{2})^2}$$

Lean4

/-- A quantity that appears in exponentials in the proof of Fernique's theorem. -/
noncomputable def logRatio (c : ℝ≥0∞) : ℝ :=
  Real.log (c.toReal / (1 - c).toReal) / (8 * (1 + √2) ^ 2)

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