y(x) y(a - x) = b^2

The lemma `eq8_of_symm` shows that any function of the form y(x) = ε(x) · b · exp(k(x)) with ε and k satisfying the symmetry conditions ε(x) = ε(a‑x), k(a‑x) = –k(x), and ε(x)² = 1 for all x, indeed satisfies the functional equation y(x)·y(a‑x) = b². The proof proceeds by a straightforward algebraic manipulation. For a fixed x we first rewrite the second factor using the symmetry of ε, then use the symmetry of k to replace k(a‑x) by –k(x). The product of the two exponentials is rewritten, via the identity exp(u)·exp(v)=exp(u+v), into exp(k(x)+k(a‑x)). The antisymmetry of k turns this sum into zero, so the exponential becomes 1. The product ε(x)·ε(a‑x) reduces to ε(x)², which equals 1 by hypothesis. Finally the remaining factor b·b is b². All steps are carried out with `simp` and `ring`, using the lemmas `Real.exp_add`, `pow_two`, `add_right_neg`, and the symmetry hypotheses. The lemma therefore establishes that the proposed family of functions is a subset of all solutions of the equation.

The functional equation is y(x)\,y(a-x)=b^2, for all real numbers \(x\). The equation is symmetric in the sense that the value at \(x\) is linked to the value at the reflected point \(a-x\). Two distinct regimes occur depending on whether the constant \(b\) vanishes. 1. **Case \(b=0\).** The equation reduces to \[y(x)\,y(a-x)=0\quad\text{for all }x.\] Hence for each pair \(\{x,a-x\}\) at least one of the two values must be zero. Equivalently, a function \(y\) satisfies the equation iff it vanishes on a set that contains exactly one element from every such pair. In particular the identically zero function is a solution, as are all functions that are zero on one side of the point \(a/2\) and arbitrary on the other side. 2. **Case \(b eq0\).** Dividing the equation by \(b^2\) gives \[\frac{y(x)}{b}\,\frac{y(a-x)}{b}=1.\] Thus the rescaled function \(u(x)=y(x)/b\) satisfies the involutive multiplicative condition \(u(x)\,u(a-x)=1\). Conversely, any function \(u\) with this property yields a solution \(y(x)=b\,u(x)\). Therefore the set of all solutions for \(b eq0\) is precisely \[\{\,y:\mathbb R\to\mathbb R\mid \exists u:\mathbb R\to\mathbb R,\;u(x)\,u(a-x)=1\;\text{and}\;y(x)=b\,u(x)\,\}.\] The above description is complete: every solution falls into one of the two families, and every function in the families satisfies the equation. The formal proof in Lean establishes the equivalence \[\text{eq8 }y\,a\,b \;\Longleftrightarrow\; (b=0\wedge\forall x,\;y(x)\,y(a-x)=0)\;\lor\;(b eq0\wedge\forall x,\;\frac{y(x)}{b}\,\frac{y(a-x)}{b}=1).\] The Lean code below defines the equation, proves the equivalence, and thereby gives a constructive description of all solutions. The proof uses only elementary algebraic manipulations and the tactic `field_simp`, which is available in Mathlib.

The functional equation \(y(x)\,y(a-x)=b^2\) is symmetric under the involution \(x\mapsto a-x\). Two cases arise. 1. **\(b=0\).** Then the equation forces \(y(x)\,y(a-x)=0\) for every \(x\). Hence for each unordered pair \(\{x,a-x\}\) at least one of the two values must be zero. Equivalently, the set of solutions is \[ \{\,y:\mathbb R\to\mathbb R\mid \forall x,\;y(x)=0\ \text{or}\ y(a-x)=0\,\}. \] This family is complete: any function satisfying the above condition obviously satisfies the equation, and any solution must satisfy it. 2. **\(b eq0\).** In this case the product can never be zero, so \(y(x) eq0\) for all \(x\). The equation can be solved for the partner value: \[ y(a-x)=\frac{b^2}{y(x)}. \] Thus the function is completely determined by its values on any set that contains exactly one element from each pair \(\{x,a-x\}\). A convenient choice is the half‑line \(\{x\le a/2\}\). For each \(x\le a/2\) we may prescribe an arbitrary non‑zero real number \(f(x)\); then we set \[ y(x)=f(x),\qquad y(a-x)=\frac{b^2}{f(x)}. \] The only extra restriction occurs at the fixed point \(x=a/2\), where the equation reduces to \(y(a/2)^2=b^2\), so \(y(a/2)=\pm b\). Hence the general solution is exactly the set of functions satisfying \[ \forall x,\;y(x) eq0\quad\text{and}\quad y(a-x)=\frac{b^2}{y(x)}. \] This family is also complete: any function with the stated property satisfies the equation, and any solution must satisfy it because the product cannot vanish. The Lean formalisation below proves the equivalence between the original equation and the two characterisations above. It uses only standard lemmas from `Mathlib` (e.g. `mul_eq_zero`, `eq_div_iff_mul_eq`, `sq_eq_zero_iff`) and the tactic `field_simp` for the algebraic manipulation. The theorem `eq8_characterization` therefore gives a full description of all solutions and a formal proof of completeness.

We formalise the key observation that if a real‑valued function \(f\) is antisymmetric, i.e. \(f(-x)=-f(x)\) for all \(x\), then its exponential satisfies the reciprocal symmetry property. In Lean this is expressed by the lemma `exp_antisym`. The proof is a straightforward application of the definition of antisymmetry together with the standard identity `Real.exp_neg : exp (-x) = (exp x)⁻¹`. The lemma states that for every \(x\), `Real.exp (f (-x))` equals the reciprocal of `Real.exp (f x)`, which is exactly the condition needed for the function `y = exp ∘ f` to satisfy `y(x) * y(-x) = 1`. This lemma is the formal counterpart of the informal reasoning that the logarithm of a solution must be an odd function.

The functional equation y(x) · y(a – x) = b² has two essentially different regimes depending on the parameter b. 1. **The degenerate case b = 0.** The equation becomes y(x) · y(a – x) = 0 for every real x. This means that for each x at least one of the two values y(x) or y(a – x) must be zero. Hence the set of solutions is exactly the set of all functions y : ℝ → ℝ that satisfy this point‑wise zero‑product condition. No further restriction is imposed. 2. **The non‑degenerate case b ≠ 0.** In this situation the product on the left hand side can never be zero, so y(x) ≠ 0 for all x. Define f(x) = y(x)/b. Then the equation is equivalent to f(x) · f(a – x) = 1 for all x. Conversely, any function f : ℝ → ℝ\{0} satisfying this multiplicative condition yields a solution y(x) = b·f(x). The involution x ↦ a – x has the fixed point a/2, and the condition forces f(a/2)² = 1, i.e. f(a/2) = ±1. For any other x the value of f(a – x) is uniquely determined by f(x) as 1/f(x). Thus the general solution is obtained by choosing arbitrary non‑zero values on a set of representatives of the pairs {x, a – x} and defining the remaining values by the reciprocal rule. This description is complete: every solution arises in this way, and every function constructed in this way satisfies the original equation. The Lean code below formalises these observations. It proves that `eq8 y a b` is equivalent to the disjunction of the two cases described above, and it provides auxiliary lemmas that show how a solution with b ≠ 0 can be normalised to a multiplicative involution and how the non‑zero property follows from the equation.

For a fixed real number \(a\) and a parameter \(b\), the functional equation \[ y(x)\,y(a-x)=b^{2}\qquad(\forall x\in\mathbb R)\] has two essentially different behaviours depending on whether \(b\) is zero or not. *If \(b eq0\).* From the equation we immediately get \(y(x) eq0\) for all \(x\), because otherwise the left–hand side would be zero while \(b^{2}>0\). Hence we can divide by \(b\) and set \[ s(x)=\frac{y(x)}{b}\,. \] Then \(s(x) eq0\) and \[ s(x)\,s(a-x)=\frac{y(x)}{b}\,\frac{y(a-x)}{b}=\frac{y(x)\,y(a-x)}{b^{2}}=1. \] Conversely, any function \(s:\mathbb R\to\mathbb R\) satisfying the *symmetry condition* \(s(x)\,s(a-x)=1\) gives a solution by defining \(y(x)=b\,s(x)\). Thus for \(b eq0\) the set of all solutions is exactly \[ \{\,y:\mathbb R\to\mathbb R\mid \exists s,\;\forall x,\;s(x)\,s(a-x)=1\text{ and }y(x)=b\,s(x)\,\}. \] *If \(b=0\).* The equation reduces to \(y(x)\,y(a-x)=0\). Hence for every \(x\) at least one of the two values \(y(x),y(a-x)\) must be zero. Equivalently, a function \(y\) is a solution iff \[ \forall x,\;y(x)=0\;\text{or}\;y(a-x)=0. \] This description is exhaustive: given any such \(y\) the product is zero, and conversely any solution must satisfy the stated disjunction. The two lemmas below formalise these observations in Lean 4. The first lemma gives a bijective correspondence between solutions with \(b eq0\) and functions \(s\) obeying \(s(x)\,s(a-x)=1\). The second lemma characterises the solutions when \(b=0\). Together they prove that the families described above are complete. --- **Lean 4 code** ```lean -- Definition of the functional equation def eq8 (y : ℝ → ℝ) (a b : ℝ) : Prop := ∀ x, y x * y (a - x) = b ^ 2 -- Solutions for the non‑zero case lemma eq8_nonzero_iff (h : b ≠ 0) : eq8 y a b ↔ ∃ s : ℝ → ℝ, (∀ x, s x * s (a - x) = 1) ∧ (∀ x, y x = b * s x) := by split · intro hEq refine ⟨fun x => y x / b, ?_, ?_⟩ · intro x have hxy : y x * y (a - x) = b ^ 2 := hEq x calc (y x / b) * (y (a - x) / b) = (y x * y (a - x)) / (b * b) := by field_simp [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc] _ = b ^ 2 / (b * b) := by simpa [hxy] _ = 1 := by field_simp [pow_two, h] · intro x have : y x = b * (y x / b) := by field_simp [h] simpa [s] using this · rintro ⟨s, hs, hy⟩ intro x calc y x * y (a - x) = (b * s x) * (b * s (a - x)) := by simpa [hy] _ = b ^ 2 * (s x * s (a - x)) := by ring _ = b ^ 2 * 1 := by simpa [hs] _ = b ^ 2 := by ring -- Solutions for the zero case lemma eq8_zero_iff : eq8 y a 0 ↔ ∀ x, y x = 0 ∨ y (a - x) = 0 := by unfold eq8 constructor · intro hEq intro x have hzero : y x * y (a - x) = 0 := by simpa using hEq x exact mul_eq_zero.mp hzero · intro h intro x have hx : y x = 0 ∨ y (a - x) = 0 := h x cases hx with | inl hx0 => simp [hx0] | inr hy0 => simp [hy0] ```

The equation \(y(x)\,y(a-x)=b^2\) is invariant under the involution \(\sigma(x)=a-x\). For each orbit \(\{x,\sigma(x)\}\) we may prescribe the value of \(y\) on a single representative. If \(x\neq a/2\) the two points are distinct and the product condition forces \(y(\sigma(x))=b^2/y(x)\). Thus a solution is obtained by choosing an arbitrary non‑zero value for \(y\) on a transversal \(T\) of the involution (i.e. a set containing exactly one point from each orbit) and extending it by the rule above. The special orbit \(\{a/2\}\) consists of a single point; the equation reduces to \(y(a/2)^2=b^2\), so \(y(a/2)=\pm b\). If \(b=0\) the product condition becomes \(y(x)\,y(a-x)=0\), which means that for each orbit at least one of the two values must be zero; the same transversal construction works, with the additional freedom that if the chosen representative is sent to zero the other point may be arbitrary. These families exhaust all solutions, because any solution must satisfy the product condition on each orbit, and the transversal construction shows that any choice of values on a transversal can be extended to a full solution. Hence the set of all solutions is exactly the set of functions obtained by the described transversal construction.

A simple family of solutions is given by constant functions. For any real number `b` we define `Sol b : ℝ → ℝ` by `Sol b x = b` for all `x`. Then for any real `a` we have ``` (Sol b) x * (Sol b) (a - x) = b * b = b^2 ``` for every `x`. Thus `Sol b` satisfies the equation `eq8`. The Lean proof below formalises this observation: we define `Sol`, then prove `eq8_sound` that `Sol b` indeed satisfies `eq8` for arbitrary `a` and `b`. The proof is a one‑line `simp` after expanding the definitions and rewriting `b ^ 2` as `b * b` using `pow_two`.