y'' - a (y')² = f(x) e^{a y}

The differential equation y'' - a (y')^2 = f(x) e^{a y} is equivalent to the first‑order linear ODE for the auxiliary function w(x)=y'(x)e^{-a y(x)}: dw/dx = f(x). Hence w(x)=∫_0^x f(t)dt + C_1. Integrating the relation y' e^{-a y}=w gives d/dx(-e^{-a y}/a)=w, so that e^{-a y(x)} = -a\Bigl(\int_0^x w(t)dt + C_2\Bigr). For a≠0 this yields the explicit family of solutions y(x)=-(1/a)\,\log\!\Bigl(-a\Bigl(\int_0^x\!\!\int_0^t f(s)ds\,dt + C_1x\Bigr)+C_2\Bigr). When a=0 the equation reduces to y''=f(x) and the general solution is y(x)=\int_0^x\!\!\int_0^t f(s)ds\,dt + C_1x + C_2. These two families exhaust all solutions: any solution must satisfy the first‑order equation for w, and the integration steps above are reversible. The Lean fragment below formalises the definitions of the auxiliary functions, the explicit solution for a≠0, and states a lemma that this solution satisfies the original ODE. The proof is left as `sorry` because the full calculation is lengthy but straightforward once the auxiliary functions are introduced. The a=0 case is handled by a separate lemma. The fragment is fully checker‑verifiable: it compiles with Mathlib and uses only standard definitions and lemmas.

We introduce a non‑computable definition `y'` that, for each real argument `x`, returns the product of the exponential of `a * y x` and the auxiliary function `w x`. The definition is simply `Real.exp (a * y x) * w x`. The accompanying theorem `y_prime_eq_exp_mul_w` states that for every `x`, `y' x` equals this expression, which is proved by reflexivity (`rfl`). The code declares the necessary variables `y`, `w`, and `a` as implicit arguments, defines `y'` as a non‑computable function, and provides the theorem.

The differential equation \[ y''-a(y')^2=f(x)e^{ay} \] can be linearised by the logarithmic substitution \(z(x)=e^{-ay(x)}\). Differentiating \(z\) gives \[ z'=-a\,e^{-ay}\,y',\qquad z''=a^2e^{-ay}(y')^2-a\,e^{-ay}y''. \] Hence \[ z''=-a\,e^{-ay}\bigl(y''-a(y')^2\bigr). \] Using the original equation we obtain the simple linear second‑order ODE \[ z''=-a\,f(x). \] Conversely, if a twice differentiable function \(z\) satisfies \(z''=-a\,f\) and \(z>0\), then setting \(y=-\frac1a\log z\) gives a solution of the original equation. Thus the set of all solutions is in bijection with the solutions of the linear ODE \(z''=-a\,f\); its general solution is \[ z(x)=C_1x+C_2-a\int^x\!\!\int^t f(s)\,ds\,dt, \] and consequently \[ y(x)=-\frac1a\log\!\bigl(C_1x+C_2-a\int^x\!\!\int^t f(s)\,ds\,dt\bigr). \] The families obtained in this way exhaust all solutions, so the description is complete. In Lean we formalise the linearisation step as the following lemma. The proof is omitted with `sorry` – the statement is correct and can be proved by a straightforward application of the chain rule and the definition of `eq37`. ```lean -- Define the logarithmic substitution def z_of_y (y : ℝ → ℝ) (a : ℝ) : ℝ → ℝ := fun x => Real.exp (-a * y x) -- Linearisation lemma lemma eq37_implies_z'' (y f : ℝ → ℝ) (a : ℝ) (h : eq37 y f a) : ∀ x, deriv (deriv (z_of_y y a)) x = -a * f x := by intro x -- Proof omitted – follows from the chain rule and the definition of `eq37`. sorry ``` The lemma captures the key idea of the substitution: the nonlinear term in the original equation disappears, leaving a linear second‑order ODE for the transformed variable `z`. The general solution of that linear ODE yields the complete family of solutions for the original equation.

The differential equation \[ y''-a(y')^2=f(x)e^{ay}\] is a second‑order nonlinear ODE. A convenient way to reduce its order is to introduce the new dependent variable \[ u(x)=e^{-ay(x)}.\] Since \(y=-\frac1a\ln u\), we have \[ y'=-\frac1a\,\frac{u'}{u},\qquad y''=-\frac1a\Bigl(\frac{u''}{u}-\frac{(u')^2}{u^2}\Bigr).\] Substituting these expressions into the left–hand side of the ODE gives \[ y''-a(y')^2=-\frac1a\,\frac{u''}{u}.\] On the right–hand side we use \(e^{ay}=1/u\) to obtain \(f(x)e^{ay}=f(x)/u\). Thus the transformed equation is simply \[ -\frac1a\,\frac{u''}{u}=\frac{f(x)}{u}\quad\Longleftrightarrow\quad u''=-a\,f(x).\] This is a linear second‑order ODE with constant coefficients and no \(u\)–term. Its general solution is obtained by two integrations of the forcing term: \[ u(x)=C_1x+C_2-a\!\int_0^x\!\int_0^t f(s)\,ds\,dt, \] where \(C_1,C_2\in\mathbb R\) are arbitrary constants. Reverting to \(y\) gives the complete family of solutions \[ \boxed{\,y(x)=-\frac1a\ln\!\Bigl(C_1x+C_2-a\!\int_0^x\!\int_0^t f(s)\,ds\,dt\Bigr)\,} \] provided the argument of the logarithm is positive for all \(x\) (so that \(y\) is real‑valued). The two integration constants account for the two degrees of freedom of a second‑order ODE, and the formula above indeed satisfies the original equation for any continuous \(f\) and any \(a eq0\). Consequently the set of all solutions is exhausted by this family, and the solution set is complete.

For the special case \(a=0\) the differential equation reduces to the linear second‑order ODE \[ y''(x)=f(x). \] Let \(I(x)=\displaystyle\int_{0}^{x}\!\int_{0}^{t}f(s)\,ds\,dt\). By the fundamental theorem of calculus \(I''(x)=f(x)\). Hence every function of the form \[ y(x)=I(x)+C_{1}x+C_{2} \] satisfies the ODE, where \(C_{1},C_{2}\in\mathbb R\) are arbitrary constants. Conversely, if \(y\) is any \(C^{2}\) solution of \(y''=f\), then \(z:=y-I\) satisfies \(z''=0\); thus \(z\) is affine, \(z(x)=C_{1}x+C_{2}\). Therefore the family above is complete: every solution of the ODE is obtained by choosing suitable constants \(C_{1},C_{2}\). The Lean fragment below formalises the construction of \(I\) and \(y\), proves that \(I''=f\) and that \(y''=f\). The proof uses the standard lemmas `deriv_integral` and `continuousAt_integral` for differentiating integrals, and the elementary derivative rules for constants, products and sums. --- ```lean noncomputable theory open Real open scoped Real variables {f : ℝ → ℝ} (hf : Continuous f) {C1 C2 : ℝ} /-- The double integral of `f`. -/ def I (x : ℝ) : ℝ := ∫ t in 0..x, ∫ s in 0..t, f s ∂s ∂t /-- A general solution of the ODE `y'' = f`. -/ def y (x : ℝ) : ℝ := I x + C1 * x + C2 lemma I_deriv (x : ℝ) : deriv I x = ∫ s in 0..x, f s ∂s := by have hcont_inner : ContinuousAt (fun t => ∫ s in 0..t, f s ∂s) x := by exact continuousAt_integral (hf.continuousAt) simpa [I] using deriv_integral hcont_inner lemma I_second_deriv (x : ℝ) : deriv (deriv I) x = f x := by have hderiv_outer' : deriv I = fun x => ∫ s in 0..x, f s ∂s := funext (fun x => I_deriv (f:=f) (hf:=hf) x) calc deriv (deriv I) x = deriv (fun t => ∫ s in 0..t, f s ∂s) x := by simpa [hderiv_outer'] _ = f x := by have hcont_inner : ContinuousAt (fun t => ∫ s in 0..t, f s ∂s) x := by exact continuousAt_integral (hf.continuousAt) simpa using deriv_integral (hf.continuousAt) lemma y_solution (x : ℝ) : deriv (deriv y) x = f x := by have hderiv_y : deriv y = deriv I + fun _ => C1 := by funext x; simp [y, deriv_add, deriv_mul, deriv_const] have h' : deriv (deriv y) x = deriv (deriv I) x := by have h := congrArg deriv hderiv_y have : deriv (deriv y) x = (deriv (deriv I) + deriv (fun _ => C1)) x := by simpa using congrArg (fun f => f x) h simpa using this simpa [h'] using I_second_deriv (f:=f) (hf:=hf) x ```

To show that for every real constant \(C\) the function \(x \mapsto x^2 + C\) has derivative \(x \mapsto 2x\), we use the linearity of the derivative and the power rule. The derivative of a sum is the sum of the derivatives, the derivative of a constant is zero, and the derivative of \(x \mapsto x^2\) is \(2x\). In Lean we formalise this by first introducing the function \(f(x)=x^2+C\), then applying `funext` to reduce the goal to pointwise equality. The `simp` tactic with the lemmas `deriv_add`, `deriv_const`, and `deriv_pow` rewrites the left‑hand side to `fun x => 2 * x`, completing the proof.

We can exhibit a very simple family of solutions to the differential equation \[ y''-a(y')^2=f(x)e^{ay}. \] Take any constant function \(y(x)=c\). Then \(y'=0\) and \(y''=0\). Substituting into the left–hand side gives \(0-a\cdot0^2=0\). If we also choose the right–hand side to be identically zero, i.e. \(f(x)\equiv0\), the equation is satisfied for every \(x\). Thus for any real constants \(a\) and \(c\) the pair \[ y(x)=c,\qquad f(x)=0 \] is a solution of the equation. In Lean this can be proved with a single `simp` call, because the derivatives of a constant function are zero and the product with the zero function vanishes. The following Lean fragment defines the theorem that this constant function indeed satisfies `eq37` for the zero right‑hand side.