Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 1 result · all verified · 1 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 1 also cleared it.

Pointwise Extended-Real Function Products

1 · Prerequisites

2 · Summary

This page defines a total pointwise product of functions from an arbitrary set into the extended real line The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined. Its zero rule includes all four ordered zero-infinity pairs. On finite inputs it is ordinary real multiplication, and on nonzero inputs with an infinite factor it follows the signs. The function-level operation leaves the existing partial scalar product unchanged and makes no measurability claim. Pointwise addition remains partial at opposite infinities, and no other extended-real scalar operation is added.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

A total pointwise product for extended-real-valued functions

Definition

Let $X$ be any set and let $f, g : X \to \overline{R}$ , where $\overline{R}$ has the order, reflection, and partial arithmetic of The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined. For each $x \in X$ , put $a = f (x)$ and $b = g (x)$ and define the value of the function $f ⊙_{X} g : X \to \overline{R}$ by these disjoint cases:

If $a = 0$ or $b = 0$ , set $(f ⊙_{X} g) (x) = 0$ .
If $a, b$ are both finite and nonzero, set $(f ⊙_{X} g) (x) = a b$ , using the real field product.
Otherwise $a, b$ are nonzero and at least one is infinite. Set $(f ⊙_{X} g) (x) = + \infty$ when $a, b$ have the same sign, and $(f ⊙_{X} g) (x) = - \infty$ when their signs differ. For a nonzero $c \in \overline{R}$ , its sign is positive when $c > 0$ and negative when $c < 0$ ; in particular $+ \infty > 0$ and $- \infty < 0$ .

This operation is defined for all functions $X \to \overline{R}$ ; no measurability of the inputs or output is asserted. It is a function-level convention and does not extend or change the partial scalar product of The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined: that scalar product remains undefined when one factor is zero and the other is infinite. Where the partial scalar product is defined, the function-level value agrees with it.

For $c \in R$ , let $\underline{c} : X \to \overline{R}$ be the constant function $\underline{c} (x) = c$ . The notation $c f$ may abbreviate the function $\underline{c} ⊙_{X} f$ ; this abbreviation refers to the function operation just defined, including when $c = 0$ and $f (x) = \pm \infty$ .

Facts & Assumptions

Given: A set $X$ and functions $f, g : X \to \overline{R}$ . Show that the clauses define exactly one value in $\overline{R}$ at every point, that the operation is symmetric, that it agrees with real multiplication on finite inputs, and that it agrees with the existing partial scalar product wherever that product is defined. Also identify the values assigned at all four zero-infinity pairs.

[F1]

The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined: $\overline{R}$ consists of the real numbers and $\pm \infty$ . Its scalar product is real multiplication on finite pairs, uses the signs of nonzero factors when an infinite factor is present, and is undefined exactly for a zero paired with $+ \infty$ or $- \infty$ .

Proof

Proof technique: partition the input values into zero, finite nonzero, and nonzero with an infinite factor.

1.1givenF1caseschoose

If $X = \emptyset$ , the unique empty function is the required output. Otherwise take any $x \in X$ and set $a = f (x)$ and $b = g (x)$ . If either is zero, only the first clause applies. If neither is zero, each is either finite or infinite by [F1]: when both are finite, only the second clause applies; otherwise at least one is infinite and only the third clause applies. Thus the cases are exhaustive and disjoint. Each clause assigns an element of $\overline{R}$ , and the nonzero values have uniquely determined signs by the total order in [F1]. Hence exactly one value is assigned at every $x$ .

1.2givenF1algebra

Swapping $a$ and $b$ leaves the zero condition and the finite-nonzero condition unchanged. The finite product is symmetric by real multiplication, and whether two signs agree is also unchanged by swapping them. Therefore $(f ⊙_{X} g) (x) = (g ⊙_{X} f) (x)$ for every $x$ , so the function operation is symmetric.

2.1givenF1step 1.1algebra

If $a, b$ are finite and one is zero, the first clause gives zero, equal to their real product. If both are finite and nonzero, the second clause is exactly their real product. Thus the operation agrees with ordinary real multiplication on all finite inputs.

3.1givenF1step 1.1step 2.1cases∎

If at least one of $a, b$ is infinite and the partial scalar product is defined, the other factor is nonzero by [F1], so the third clause gives exactly the sign-rule value of that partial product. Its only undefined value pairs are $(0, + \infty)$ , $(0, - \infty)$ , $(+ \infty, 0)$ , and $(- \infty, 0)$ ; the function operation assigns zero to each by its first clause. This verifies the agreement where defined and records all four additional function-level values.

Remarks

The symbol $⊙_{X}$ denotes a convention for pointwise function formulas. It does not make $\overline{R}$ a field, create distributivity or cancellation laws at infinite values, or specify a rule for products of limits. The existing pointwise sum remains partial when opposite infinities meet; no subtraction, division, exponentiation, or absolute-value operation on $\overline{R}$ is added. A difference written as $u + (- v)$ still requires that this partial sum be defined. No axiom of choice is used: the value at each point is determined directly by the two input values.

5 · Examples, counterexamples and false statements

None yet.