English
Real-valued density case of the decomposition into positive/negative parts using ENNReal.ofReal.
Русский
Случай для действительной плотности разложения на положительные/отрицательные части через ENNReal.ofReal.
LaTeX
$$$\mu.withDensityᵥ f = \mathrm{toSignedMeasure}(\mu.withDensity (x \mapsto ENNReal.ofReal(f(x)))) - \mathrm{toSignedMeasure}(\mu.withDensity (x \mapsto ENNReal.ofReal(-f(x))))$$$
Lean4
/-- The Proposition corresponding to each field axiom -/
@[simp]
def toProp (K : Type*) [Add K] [Mul K] [Neg K] [Zero K] [One K] : FieldAxiom → Prop
| .addAssoc => ∀ x y z : K, (x + y) + z = x + (y + z)
| .zeroAdd => ∀ x : K, 0 + x = x
| .negAddCancel => ∀ x : K, -x + x = 0
| .mulAssoc => ∀ x y z : K, (x * y) * z = x * (y * z)
| .mulComm => ∀ x y : K, x * y = y * x
| .oneMul => ∀ x : K, 1 * x = x
| .existsInv => ∀ x : K, x ≠ 0 → ∃ y, x * y = 1
| .leftDistrib => ∀ x y z : K, x * (y + z) = x * y + x * z
| .existsPairNE => ∃ x y : K, x ≠ y
