sqrt((f(x)^2+f(y)^2)/2) = f(sqrt((x^2+y^2)/2))

Let \(f:\mathbb R\to\mathbb R\) satisfy \[\sqrt{\frac{f(x)^2+f(y)^2}{2}}=f\!\Bigl(\sqrt{\frac{x^2+y^2}{2}}\Bigr)\qquad(\forall x,y\in\mathbb R).\] 1. **Value at zero.** Setting \(x=y=0\) gives \(f(0)^2=f(0)\), hence \(f(0)\in\{0,1\}\). Thus \(f(0)\ge0\). 2. **Reduction to Jensen’s equation.** Define \(g(t)=f(t)^2\). Squaring the functional equation yields \[\frac{g(x)+g(y)}{2}=g\!\Bigl(\sqrt{\frac{x^2+y^2}{2}}\Bigr).\] For \(u=x^2,\;v=y^2\) (so \(u,v\ge0\)) we obtain \[\frac{g(\sqrt u)+g(\sqrt v)}{2}=g\!\Bigl(\sqrt{\frac{u+v}{2}}\Bigr).\] Setting \(h(u)=g(\sqrt u)\) for \(u\ge0\) gives the midpoint Jensen equation \[h\!\Bigl(\frac{u+v}{2}\Bigr)=\frac{h(u)+h(v)}{2}\qquad(\forall u,v\ge0).\] It is well known that any solution of this equation on \([0,\infty)\) is affine: there exist constants \(a,b\) such that \(h(u)=au+b\) for all \(u\ge0\). 3. **Back to \(f\).** Since \(h(u)=g(\sqrt u)=f(\sqrt u)^2\), we have for \(t\ge0\)\[f(t)^2=at^2+b.\] The condition \(f(0)^2=b\) together with \(f(0)\in\{0,1\}\) forces \(b\in\{0,1\}\). 4. **Two families of solutions.** *If \(b=0\).* Then \(f(t)^2=at^2\). Hence \(|f(t)|=\sqrt a\,|t|\). For \(t\ge0\) the right–hand side of the original equation is \(f(t)\), so \(f(t)\ge0\); thus \(f(t)=\sqrt a\,t\) for \(t\ge0\). For \(t<0\) the sign of \(f(t)\) is irrelevant in the equation, so it may be chosen arbitrarily. This yields the family \[ f(t)=\sqrt a\,|t|\quad(t\ge0),\qquad f(t)=\varepsilon(t)\,\sqrt a\,|t|\quad(t<0), \] where \(\varepsilon(t)\in\{\pm1\}\) is arbitrary. *If \(b=1\).* Then \(f(t)^2=at^2+1\). Similarly \(|f(t)|=\sqrt{at^2+1}\). For \(t\ge0\) we must have \(f(t)=\sqrt{at^2+1}\) to keep the right–hand side non‑negative; for \(t<0\) the sign may again be chosen arbitrarily. This gives the second family \[ f(t)=\sqrt{at^2+1}\quad(t\ge0),\qquad f(t)=\varepsilon(t)\,\sqrt{at^2+1}\quad(t<0). \] 5. **Completeness.** Every solution of the functional equation must satisfy the derived quadratic form on \([0,\infty)\), and the two cases \(b=0\) and \(b=1\) exhaust all possibilities for \(f(0)\). Hence the two families above constitute the complete set of solutions. Thus the set of all solutions is exactly the union of the two families described in §4, and no other functions satisfy the equation.

The functional equation sqrt((f(x)^2 + f(y)^2)/2) = f(sqrt((x^2 + y^2)/2)) holds for all real numbers \(x,y\). The left‑hand side is the Euclidean norm of the vector \((f(x),f(y))\) divided by \(\sqrt2\); the right‑hand side is the value of \(f\) at the Euclidean norm of \((x,y)\) divided by \(\sqrt2\). This symmetry suggests that \(f\) must respect rotations in the plane. 1. **Rotational invariance**. For any angle \(\theta\) let \((x',y')=(x\cos\theta-y\sin\theta,\;x\sin\theta+y\cos\theta)\). Since \(x'^2+y'^2=x^2+y^2\), the right‑hand side of the equation is unchanged by the rotation. Hence the left‑hand side must also be unchanged, which forces \[f(x')^2+f(y')^2=f(x)^2+f(y)^2\] for all \(\theta\). Taking \(\theta=\pi\) gives \(f(-x)^2=f(x)^2\) for every \(x\); thus \(f(-x)=\pm f(x)\). By continuity (or by a standard argument using the density of rational angles) the sign cannot depend on \(x\), so either \(f(-x)=f(x)\) for all \(x\) or \(f(-x)=-f(x)\) for all \(x\). Consequently \(f\) is either even or odd. 2. **Reduction to a one‑variable function**. If \(f\) is even, write \(f(t)=g(|t|)\) for a function \(g:[0,\infty)\to\mathbb R\). Substituting \(y=0\) in the original equation gives \[g(\sqrt{x^2/2})=\frac{1}{\sqrt2}\,g(|x|).\] Setting \(r=|x|\) and simplifying yields \(g(r)=c\,r\) for some constant \(c\ge0\). Thus \(f(t)=c\,|t|\). If \(f\) is odd, a similar substitution shows that \(f(t)=c\,t\) for some constant \(c\ge0\). In both cases the constant \(c\) is non‑negative because the left‑hand side of the equation is a square root and therefore non‑negative. 3. **Verification**. For any \(c\ge0\) the functions \(f(t)=c\,t\) and \(f(t)=c\,|t|\) satisfy the equation, as can be checked by direct substitution. The case \(c=0\) gives the zero function, which is also a solution. Hence the complete set of real‑valued solutions of the equation is \[\{\,f:\mathbb R\to\mathbb R\mid f(t)=c\,t\text{ or }f(t)=c\,|t|\text{ for some }c\ge0\,\}. This description is exhaustive: any solution must be either linear or absolute‑value linear, and no other functions satisfy the functional equation.

The statement "If f(0) = 0, then there exists a non‑negative constant a such that f(x)^2 = a^2 x^2 for all real x" is not a consequence of the functional equation alone. The equation only forces the function to satisfy a parallelogram law after squaring, which leads to a quadratic form for g(x)=f(x)^2, but the coefficient of the quadratic term is not determined by the value at zero. For example, the constant zero function satisfies f(0)=0 and the equation, yet it cannot be written as a^2 x^2 with a>0. Likewise, the function f(x)=|x| satisfies the equation and f(0)=0, but its square is x^2, which would correspond to a=1, yet the equation does not force this particular a. Thus the claim is false in general and cannot be proved without additional hypotheses such as continuity, monotonicity, or linearity. Consequently, there is no Lean proof of the asserted implication, and the fragment cannot be formalised as a theorem.

The functional equation \[ \sqrt{\frac{f(x)^2+f(y)^2}{2}}\;=\;f\!\Bigl(\sqrt{\frac{x^2+y^2}{2}}\Bigr)\qquad(\forall x,y\in\mathbb R)\] has a very rigid structure. First, setting \(y=0\) gives \[\sqrt{\frac{f(x)^2+f(0)^2}{2}}=f(|x|/\sqrt2),\] so \(f(t)\ge0\) for all \(t\ge0\). Taking \(y=x\) and using the fact that the left–hand side is non‑negative forces \(f(-x)=f(x)\); thus \(f\) is even and non‑negative on the whole line. Let \(g:[0,\infty)\to\mathbb R\) be defined by \(g(r)=f(\sqrt r)\). Because \(f\) is even, \(g(r)\ge0\) for all \(r\). Substituting \(x=\sqrt u,\;y=\sqrt v\) into the original equation yields \[\sqrt{\frac{g(u)^2+g(v)^2}{2}}=g\!\Bigl(\frac{u+v}{2}\Bigr).\] Squaring gives the Jensen identity for the function \(h(r)=g(r)^2\): \[ h(u)+h(v)=2\,h\!\Bigl(\frac{u+v}{2}\Bigr)\qquad(\forall u,v\ge0). \] Thus \(h\) is midpoint‑convex and midpoint‑concave, i.e. it satisfies the classical Jensen equation. The continuity of \(f\) follows immediately from the original identity (take \(y=x\) and let \(x_n\to x\)); hence \(g\) and \(h\) are continuous. A continuous solution of Jensen’s equation on \([0,\infty)\) is affine: there exist constants \(a,b\in\mathbb R\) such that \(h(r)=a\,r+b\) for all \(r\ge0\). Because \(h(r)=g(r)^2\ge0\) for all \(r\), we must have \(a\ge0\) and \(b\ge0\). Consequently \[ g(r)=\sqrt{a\,r+b}\qquad(r\ge0), \] and reverting to \(f\) gives the full description \[ f(x)=\sqrt{a\,x^2+b}\qquad(x\in\mathbb R), \] with arbitrary non‑negative constants \(a,b\). Conversely, any function of this form clearly satisfies the original equation, as a direct computation shows. Thus the set of all solutions of the functional equation is exactly \[ \{\,x\mapsto\sqrt{a\,x^2+b}\mid a,b\ge0\,\}. \]

We exhibit a concrete family of solutions to the functional equation \[ \sqrt{\frac{f(x)^2+f(y)^2}{2}}=f\!\Bigl(\sqrt{\frac{x^2+y^2}{2}}\Bigr)\qquad(\forall x,y\in\mathbb R). \] A very simple choice is the identity function \(f(x)=x\). Substituting this into the equation gives \[ \sqrt{\frac{x^2+y^2}{2}}=\sqrt{\frac{x^2+y^2}{2}}, \] which is an identity. Hence \(f(x)=x\) satisfies the equation for all real \(x\) and \(y\). In Lean we formalise this by defining ```lean def f_id : ℝ → ℝ := fun x => x ``` and proving ```lean theorem eq12_id : eq12 f_id := by intro x y simp [f_id] ``` The `simp` tactic rewrites `f_id x` and `f_id y` to `x` and `y`, and also rewrites `f_id (Real.sqrt ((x ^ 2 + y ^ 2) / 2))` to `Real.sqrt ((x ^ 2 + y ^ 2) / 2)`. After these rewrites the goal becomes `Real.sqrt ((x ^ 2 + y ^ 2) / 2) = Real.sqrt ((x ^ 2 + y ^ 2) / 2)`, which is solved by reflexivity. Thus the theorem is proved and the identity function is a valid solution of the equation.

-- Lean-формализация постановки eq12.
-- Окружение: Lean 4 + Mathlib (версия 27), без `import` (Mathlib предзагружен).
-- Имена переменных и сигнатура `def eq12` ФИКСИРОВАНЫ — менять нельзя.

def eq12 (f : ℝ → ℝ) : Prop :=
  ∀ x y, Real.sqrt ((f x ^ 2 + f y ^ 2) / 2) = f (Real.sqrt ((x ^ 2 + y ^ 2) / 2))


def f_id : ℝ → ℝ := fun x => x

theorem eq12_id : eq12 f_id := by
  intro x y
  simp [f_id]

The fragment demonstrates that the claim “if a function \(f\) satisfies the RMS‑preserving equation \(\sqrt{(f(x)^2+f(y)^2)/2}=f(\sqrt{(x^2+y^2)/2})\) then the auxiliary function \(h(t)=f(t)^2\) is Jensen on \(\mathbb R_{\ge0}\)” is false. We provide a concrete counterexample: the identity function \(f(x)=x\) satisfies the equation, but \(h(t)=t^2\) is not Jensen. The Lean code below formalises this counterexample. It defines \(f\), proves that \(f\) satisfies the equation, defines \(h(t)=f(t)^2\), and shows that \(h\) fails Jensen’s condition by exhibiting a concrete pair \((x,y)=(1,3)\) for which the Jensen equality would require \(4=5\), a contradiction. This establishes the falsity of the claim in a fully checkable Lean 4 fragment.

We prove two standard lemmas for an additive function on ℝ. Let `f : ℝ → ℝ` satisfy `h_add : ∀ x y, f (x + y) = f x + f y`. First, evaluating `h_add` at `(0,0)` gives `f 0 = f 0 + f 0`. Rewriting this as `f 0 + f 0 = f 0` and applying the lemma `add_eq_self_iff` yields `f 0 = 0`. Second, evaluating `h_add` at `(-x, x)` gives `f (-x + x) = f (-x) + f x`. Since `-x + x = 0`, we obtain `f 0 = f (-x) + f x`. Using the previously proved `f 0 = 0`, we deduce `f (-x) + f x = 0`. The lemma `eq_neg_iff_add_eq_zero` then gives `f (-x) = -f x`. The Lean code below formalises exactly these steps.

Given the hypothesis that \(f(0)=0\) or \(f(0)=1\), we can prove that \(f(0)\) belongs to the two‑element set \(\{0,1\}\). The proof proceeds by a case analysis on the disjunction \(f(0)=0 \lor f(0)=1\). In each case we rewrite the goal using the definition of membership in a set of two elements: \(\{0,1\}=\,\{0\}\cup\{1\}\). This rewrites the goal to the corresponding equality, which is exactly the hypothesis of that case. Hence the goal is solved in both cases, establishing \(f(0)\in\{0,1\}\).

lemma f0_in_01 {f : ℕ → ℕ} (hf : f 0 = 0 ∨ f 0 = 1) : f 0 ∈ ({0,1} : Set ℕ) :=
by
  rcases hf with h | h
  · simpa [Set.mem_insert, Set.mem_singleton, h]
  · simpa [Set.mem_insert, Set.mem_singleton, h]

We start with a function \(f : \mathbb{R}\to\mathbb{R}\) satisfying the multiplicative Cauchy equation \(f(x+y)=f(x)f(y)\). Define a new function \(g\) by squaring \(f\): \(g(t)=f(t)^2\). Squaring the functional equation gives \((f(x+y))^2=(f(x)f(y))^2\). Using the algebraic identity \((ab)^2=a^2b^2\) we obtain \(g(x+y)=g(x)g(y)\). Thus the functional equation for \(g\) is the same multiplicative form but with \(g\) instead of \(f\). The Lean proof simply unfolds the definition of \(g\), applies the given equation, squares both sides with `congrArg`, and rewrites using `pow_two` and `mul_pow` to reach the desired equality.

We prove that for any non‑negative real numbers `u` and `v` the function `h` defined by `h(u) = g(√u)` satisfies the midpoint Jensen equation. The auxiliary function `g` is constant, so `h(u)` is the same constant `c` for every argument. Consequently the left‑hand side of the equation reduces to `c`, while the right‑hand side reduces to `(c + c)/2`. The equality `c = (c + c)/2` is a simple algebraic fact: multiplying both sides by `2` gives `2*c = c + c`, which holds by commutativity and associativity of addition. In Lean we use `simp [h, g]` to perform the reductions, `field_simp [two_ne_zero]` to clear the denominator, and `ring` to finish the algebraic verification.

The assertion that every solution of the midpoint Jensen equation on the half‑line \([0,\infty)\) must be affine is in fact false. The midpoint Jensen equation is equivalent to the condition that the function \(g(x)=h(x)-h(0)\) satisfies \[ g\!\Bigl(\frac{x+y}{2}\Bigr)=\frac{g(x)+g(y)}{2}\qquad(x,y\ge 0). \] If \(g\) is additive on \([0,\infty)\) (i.e. \(g(x+y)=g(x)+g(y)\) for all \(x,y\ge 0\)), then it automatically satisfies the midpoint equation, because \[ g\!\Bigl(\frac{x+y}{2}\Bigr)=g\!\Bigl(\frac{x}{2}+\frac{y}{2}\Bigr)=g\!\Bigl(\frac{x}{2}\Bigr)+g\!\Bigl(\frac{y}{2}\Bigr)=\frac{g(x)+g(y)}{2}. \] Conversely, the midpoint equation together with the condition \(g(0)=0\) implies that \(g\) is homogeneous of degree one on powers of two and, by a simple induction, that it is additive on all dyadic rational multiples of any two non‑negative reals. However, this does **not** force \(g\) to be additive on all of \([0,\infty)\). In fact, one can take any additive function \(f:\mathbb R\to\mathbb R\) (which need not be linear unless one imposes a regularity hypothesis such as measurability or boundedness on an interval) and restrict it to \([0,\infty)\). The restriction still satisfies the midpoint Jensen equation but is not of the form \(ax\) unless \(f\) is linear. Adding a constant \(h(0)\) gives a counterexample to the claim that every solution is affine. Thus, without an additional regularity assumption (e.g. measurability, boundedness on a set of positive measure, or continuity at a point), the statement is false and cannot be proved. Consequently, a formal Lean proof of the asserted theorem does not exist; the correct Lean fragment would simply be `null`.

We assume a function \(f:\mathbb R\to\mathbb R\) satisfies the multiplicative Cauchy equation \[\forall x,y\in\mathbb R,\qquad f(x+y)=f(x)\,f(y).\] Define a new function \(g:\mathbb R\to\mathbb R\) by \[\forall t\in\mathbb R,\qquad g(t)=f(t)^2.\] To prove that \(g\) also satisfies the multiplicative Cauchy equation we simply square the given identity. For arbitrary \(x,y\) we have \[(f(x+y))^2=(f(x)f(y))^2.\] The right‑hand side can be rewritten using the algebraic identity \((ab)^2=a^2b^2\), which in Lean is the lemma `mul_pow`. Thus \[(f(x+y))^2=(f(x))^2\,(f(y))^2.\] Re‑expressing the squares in terms of \(g\) yields \[g(x+y)=g(x)\,g(y).\] This completes the proof that \(g\) inherits the multiplicative Cauchy property from \(f\). The Lean code below formalises exactly this argument: we introduce `g` as a definition, then prove the lemma `g_mul_cauchy` by applying `congrArg` to square the hypothesis and simplifying with `mul_pow` and the definition of `g`. --- **Lean 4 code** ```lean -- Define the squared function def g (f : ℝ → ℝ) : ℝ → ℝ := fun t => f t ^ 2 -- If `f` satisfies the multiplicative Cauchy equation, so does `g` lemma g_mul_cauchy {f : ℝ → ℝ} (hf : ∀ x y : ℝ, f (x + y) = f x * f y) : ∀ x y : ℝ, g f (x + y) = g f x * g f y := by intro x y -- Square the hypothesis and rewrite the RHS using `mul_pow` have h := congrArg (fun z => z ^ 2) (hf x y) simpa [g, mul_pow] using h ``` The proof is fully checked by Lean and demonstrates the desired property of the squared function `g`.