IndisputableMonolith.Cost.AczelProof
IndisputableMonolith/Cost/AczelProof.lean · 415 lines · 16 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Cost.AczelClass
3import IndisputableMonolith.Cost.AczelTheorem
4import IndisputableMonolith.Cost.FunctionalEquation
5
6/-!
7# Proof of Aczél's Smoothness Theorem
8
9Any continuous solution H : ℝ → ℝ of the d'Alembert functional equation
10 H(t + u) + H(t - u) = 2 · H(t) · H(u)
11with H(0) = 1 is real analytic (ContDiff ℝ ⊤).
12
13The proof:
141. **Integration bootstrap**: Continuous → C^∞ via an antiderivative representation.
152. **ODE derivation**: C^∞ + d'Alembert ⟹ H'' = c·H for c = H''(0).
163. **Classification**: Identify H as cosh(λ·), cos(λ·), or 1; conclude analyticity.
17
18Reference: Aczél, "Lectures on Functional Equations" (1966), Chapter 3.
19-/
20
21namespace IndisputableMonolith.Cost.FunctionalEquation
22
23open Real MeasureTheory
24
25noncomputable section
26
27private abbrev smooth : WithTop ℕ∞ := (⊤ : ℕ∞)
28
29/-! ## Phase 1: Integration Bootstrap (Continuous → C^∞) -/
30
31private def Phi (H : ℝ → ℝ) (t : ℝ) : ℝ := ∫ s in (0 : ℝ)..t, H s
32
33private lemma phi_zero (H : ℝ → ℝ) : Phi H 0 = 0 := by
34 simp [Phi, intervalIntegral.integral_same]
35
36private lemma phi_hasDerivAt (H : ℝ → ℝ) (h_cont : Continuous H) (t : ℝ) :
37 HasDerivAt (Phi H) (H t) t :=
38 intervalIntegral.integral_hasDerivAt_right (h_cont.intervalIntegrable 0 t)
39 h_cont.aestronglyMeasurable.stronglyMeasurableAtFilter h_cont.continuousAt
40
41private lemma phi_differentiable (H : ℝ → ℝ) (h_cont : Continuous H) :
42 Differentiable ℝ (Phi H) :=
43 fun t => (phi_hasDerivAt H h_cont t).differentiableAt
44
45private lemma deriv_phi_eq (H : ℝ → ℝ) (h_cont : Continuous H) : deriv (Phi H) = H :=
46 funext fun t => (phi_hasDerivAt H h_cont t).deriv
47
48private lemma exists_integral_ne_zero (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H) :
49 ∃ δ : ℝ, 0 < δ ∧ Phi H δ ≠ 0 := by
50 have h_pos : (0 : ℝ) < H 0 := by rw [h_one]; exact one_pos
51 have h_ev : ∀ᶠ x in nhds (0 : ℝ), (0 : ℝ) < H x :=
52 h_cont.continuousAt.eventually (Ioi_mem_nhds h_pos)
53 obtain ⟨ε, hε_pos, hε⟩ := Metric.eventually_nhds_iff.mp h_ev
54 refine ⟨ε / 2, by positivity, ?_⟩
55 intro h_eq
56 have hδ_pos : (0 : ℝ) < ε / 2 := by positivity
57 obtain ⟨c, hc_mem, hc_eq⟩ := exists_hasDerivAt_eq_slope (Phi H) H hδ_pos
58 ((phi_differentiable H h_cont).continuous.continuousOn)
59 (fun x _ => phi_hasDerivAt H h_cont x)
60 rw [phi_zero, h_eq, sub_zero, zero_div] at hc_eq
61 linarith [hε (show dist c 0 < ε by
62 simp only [Real.dist_eq, sub_zero, abs_of_pos hc_mem.1]; linarith [hc_mem.2])]
63
64private lemma representation_formula (H : ℝ → ℝ) (h_cont : Continuous H)
65 (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u)
66 {δ : ℝ} (hδ_ne : Phi H δ ≠ 0) (t : ℝ) :
67 H t = (Phi H (t + δ) - Phi H (t - δ)) / (2 * Phi H δ) := by
68 -- Strategy: avoid integral substitution by using FTC + is_const_of_deriv_eq_zero.
69 -- We prove ∫₀ᵈ H(t+u)du = Phi(t+d)-Phi(t) and ∫₀ᵈ H(t-u)du = Phi(t)-Phi(t-d)
70 -- by showing both sides have the same derivative (w.r.t. d) and agree at d=0.
71 -- Then the d'Alembert equation integrated gives the representation.
72 have h_cont_add : Continuous (fun u => H (t + u)) :=
73 h_cont.comp (continuous_const.add continuous_id)
74 have h_cont_sub : Continuous (fun u => H (t - u)) :=
75 h_cont.comp (continuous_const.sub continuous_id)
76 -- Step 1: ∫₀ᵈ H(t+u) du = Phi(t+d) - Phi(t)
77 -- Proof: define F(d) = LHS - RHS, show F'=0 and F(0)=0, so F=0.
78 have h_shift : ∀ d, ∫ u in (0:ℝ)..d, H (t + u) = Phi H (t + d) - Phi H t := by
79 intro d
80 let F : ℝ → ℝ := fun d => (∫ u in (0:ℝ)..d, H (t + u)) - (Phi H (t + d) - Phi H t)
81 suffices hF : F d = 0 by simp only [F] at hF; linarith
82 have hF_hasDerivAt : ∀ d, HasDerivAt F 0 d := by
83 intro d
84 have h1 := intervalIntegral.integral_hasDerivAt_right
85 (h_cont_add.intervalIntegrable 0 d)
86 h_cont_add.aestronglyMeasurable.stronglyMeasurableAtFilter
87 h_cont_add.continuousAt
88 have h2_raw := (phi_hasDerivAt H h_cont (t + d)).comp d ((hasDerivAt_id d).const_add t)
89 have h2 : HasDerivAt (fun d => Phi H (t + d)) (H (t + d)) d := by
90 simpa only [mul_one, Function.comp_def] using h2_raw
91 show HasDerivAt F 0 d
92 have h3 : HasDerivAt F (H (t + d) - H (t + d)) d := h1.sub (h2.sub_const _)
93 simpa using h3
94 have hF0 : F 0 = 0 := by simp [F, intervalIntegral.integral_same, phi_zero]
95 have hF_diff : Differentiable ℝ F := fun d => (hF_hasDerivAt d).differentiableAt
96 have hF_const := is_const_of_deriv_eq_zero hF_diff (fun d => (hF_hasDerivAt d).deriv)
97 linarith [hF_const d 0]
98 -- Step 2: ∫₀ᵈ H(t-u) du = Phi(t) - Phi(t-d)
99 have h_refl : ∀ d, ∫ u in (0:ℝ)..d, H (t - u) = Phi H t - Phi H (t - d) := by
100 intro d
101 let F : ℝ → ℝ := fun d => (∫ u in (0:ℝ)..d, H (t - u)) - (Phi H t - Phi H (t - d))
102 suffices hF : F d = 0 by simp only [F] at hF; linarith
103 have hF_hasDerivAt : ∀ d, HasDerivAt F 0 d := by
104 intro d
105 have h1 := intervalIntegral.integral_hasDerivAt_right
106 (h_cont_sub.intervalIntegrable 0 d)
107 h_cont_sub.aestronglyMeasurable.stronglyMeasurableAtFilter
108 h_cont_sub.continuousAt
109 have h_neg_raw := (hasDerivAt_id d).const_sub t
110 have h_neg : HasDerivAt (fun d => t - d) (-1) d := by simpa using h_neg_raw
111 have h_comp := (phi_hasDerivAt H h_cont (t - d)).comp d h_neg
112 have h2 : HasDerivAt (fun d => Phi H t - Phi H (t - d)) (H (t - d)) d := by
113 have h_phi_td : HasDerivAt (fun d => Phi H (t - d)) (H (t - d) * (-1)) d := by
114 simpa only [Function.comp_def] using h_comp
115 convert (hasDerivAt_const d (Phi H t)).sub h_phi_td using 1; ring
116 show HasDerivAt F 0 d
117 have h3 : HasDerivAt F (H (t - d) - H (t - d)) d := h1.sub h2
118 simpa using h3
119 have hF0 : F 0 = 0 := by simp [F, intervalIntegral.integral_same, phi_zero, sub_zero]
120 have hF_diff : Differentiable ℝ F := fun d => (hF_hasDerivAt d).differentiableAt
121 have hF_const := is_const_of_deriv_eq_zero hF_diff (fun d => (hF_hasDerivAt d).deriv)
122 linarith [hF_const d 0]
123 -- Step 3: Combine via d'Alembert
124 have h_add_int : IntervalIntegrable (fun u => H (t + u)) volume 0 δ :=
125 h_cont_add.intervalIntegrable 0 δ
126 have h_sub_int : IntervalIntegrable (fun u => H (t - u)) volume 0 δ :=
127 h_cont_sub.intervalIntegrable 0 δ
128 have h_integral : Phi H (t + δ) - Phi H (t - δ) = 2 * H t * Phi H δ := by
129 have h1 := h_shift δ
130 have h2 := h_refl δ
131 have h3 : (∫ u in (0:ℝ)..δ, H (t + u)) + (∫ u in (0:ℝ)..δ, H (t - u)) =
132 2 * H t * Phi H δ := by
133 rw [← intervalIntegral.integral_add h_add_int h_sub_int]
134 simp_rw [show ∀ u, H (t + u) + H (t - u) = 2 * H t * H u from h_dAl t]
135 exact intervalIntegral.integral_const_mul (2 * H t) H
136 linarith
137 field_simp at h_integral ⊢; linarith
138
139private lemma phi_contDiff_succ (H : ℝ → ℝ) (h_cont : Continuous H) {n : ℕ}
140 (h : ContDiff ℝ (n : ℕ∞) H) : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞) (Phi H) := by
141 suffices ContDiff ℝ ((n : ℕ∞) + 1) (Phi H) by exact_mod_cast this
142 rw [contDiff_succ_iff_deriv]
143 exact ⟨phi_differentiable H h_cont,
144 fun h_omega => absurd h_omega (by exact_mod_cast WithTop.coe_ne_top),
145 by rwa [deriv_phi_eq H h_cont]⟩
146
147private theorem dAlembert_contDiff_nat (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H)
148 (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
149 ∀ n : ℕ, ContDiff ℝ (n : ℕ∞) H := by
150 obtain ⟨δ, _, hδ_ne⟩ := exists_integral_ne_zero H h_one h_cont
151 have h_rep := representation_formula H h_cont h_dAl hδ_ne
152 intro n; induction n with
153 | zero => exact contDiff_zero.mpr h_cont
154 | succ n ih =>
155 have h_phi := phi_contDiff_succ H h_cont ih
156 have h1 : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞) (fun t => Phi H (t + δ)) :=
157 h_phi.comp (contDiff_id.add contDiff_const)
158 have h2 : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞) (fun t => Phi H (t - δ)) :=
159 h_phi.comp (contDiff_id.sub contDiff_const)
160 have h4 : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞)
161 (fun t => (Phi H (t + δ) - Phi H (t - δ)) / (2 * Phi H δ)) :=
162 (h1.sub h2).div_const _
163 exact (funext h_rep) ▸ h4
164
165private theorem dAlembert_contDiff_smooth (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H)
166 (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
167 ContDiff ℝ smooth H :=
168 contDiff_infty.mpr (dAlembert_contDiff_nat H h_one h_cont h_dAl)
169
170/-! ## Phase 2: General ODE Derivation -/
171
172private theorem dAlembert_to_ODE_general (H : ℝ → ℝ)
173 (h_smooth : ContDiff ℝ smooth H)
174 (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
175 ∀ t, deriv (deriv H) t = deriv (deriv H) 0 * H t := by
176 have h2 : ContDiff ℝ 2 H := by exact_mod_cast (contDiff_infty.mp h_smooth) 2
177 have hDiff : Differentiable ℝ H := h2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
178 have hCDiff1_H' : ContDiff ℝ 1 (deriv H) := by
179 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h2
180 rw [contDiff_succ_iff_deriv] at h2; exact h2.2.2
181 have hDiffDeriv : Differentiable ℝ (deriv H) :=
182 hCDiff1_H'.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
183 have hsh_add : ∀ (s v : ℝ), HasDerivAt (fun u => s + u) (1 : ℝ) v := fun s v => by
184 have h := (hasDerivAt_id v).add_const s; simp only [id] at h
185 rwa [show (fun u : ℝ => u + s) = fun u => s + u from funext fun u => add_comm u s] at h
186 have hsh_sub : ∀ (s v : ℝ), HasDerivAt (fun u => s - u) (-1 : ℝ) v := fun s v => by
187 have h1 : HasDerivAt (fun u : ℝ => -u) (-1 : ℝ) v := by
188 have := (hasDerivAt_id v).neg; simp only [id] at this; exact this
189 have h2 := h1.const_add s
190 rwa [show (fun u : ℝ => s + -u) = fun u => s - u from funext fun u => by ring] at h2
191 intro t
192 have h_feq : (fun u => H (t + u) + H (t - u)) = (fun u => 2 * H t * H u) :=
193 funext (h_dAl t)
194 have key : deriv (deriv (fun u => H (t + u) + H (t - u))) 0 =
195 deriv (deriv (fun u => 2 * H t * H u)) 0 :=
196 congr_arg (fun f => deriv (deriv f) 0) h_feq
197 have lhs_eq : deriv (deriv (fun u => H (t + u) + H (t - u))) 0 =
198 2 * deriv (deriv H) t := by
199 have h_plus : ∀ v, HasDerivAt (fun u => H (t + u)) (deriv H (t + v)) v := fun v => by
200 have h := ((hDiff (t + v)).hasDerivAt).comp v (hsh_add t v)
201 simp only [mul_one, Function.comp_def] at h; exact h
202 have h_minus : ∀ v, HasDerivAt (fun u => H (t - u)) (-deriv H (t - v)) v := fun v => by
203 have hcomp := ((hDiff (t - v)).hasDerivAt).comp v (hsh_sub t v)
204 simp only [mul_neg, mul_one, Function.comp_apply] at hcomp; exact hcomp
205 have hfirst : deriv (fun u => H (t + u) + H (t - u)) =
206 fun v => deriv H (t + v) - deriv H (t - v) := funext fun v => by
207 have h12 := ((h_plus v).add (h_minus v)).deriv
208 rw [show (fun u => H (t + u)) + (fun u => H (t - u)) =
209 fun u => H (t + u) + H (t - u) from by ext u; rfl] at h12; linarith [h12]
210 have hd2p : HasDerivAt (fun v => deriv H (t + v)) (deriv (deriv H) t) 0 := by
211 have := ((hDiffDeriv (t + 0)).hasDerivAt).comp 0 (hsh_add t 0)
212 simpa using this
213 have hd2m : HasDerivAt (fun v => deriv H (t - v)) (-deriv (deriv H) t) 0 := by
214 have := ((hDiffDeriv (t - 0)).hasDerivAt).comp 0 (hsh_sub t 0)
215 simpa using this
216 rw [congr_fun (congr_arg deriv hfirst) 0,
217 show (fun v => deriv H (t + v) - deriv H (t - v)) =
218 (fun v => deriv H (t + v)) - (fun v => deriv H (t - v)) from rfl]
219 linarith [(hd2p.sub hd2m).deriv]
220 have rhs_eq : deriv (deriv (fun u => 2 * H t * H u)) 0 =
221 2 * H t * deriv (deriv H) 0 := by
222 have hf : deriv (fun u => 2 * H t * H u) = fun v => 2 * H t * deriv H v :=
223 funext fun v => ((hDiff v).hasDerivAt.const_mul (2 * H t)).deriv
224 rw [congr_fun (congr_arg deriv hf) 0, ((hDiffDeriv 0).hasDerivAt.const_mul (2 * H t)).deriv]
225 rw [lhs_eq, rhs_eq] at key; linarith
226
227/-! ## Phase 3: Classification and Analyticity -/
228
229private theorem ode_neg_zero_uniqueness (f : ℝ → ℝ)
230 (h_diff2 : ContDiff ℝ 2 f)
231 (h_ode : ∀ t, deriv (deriv f) t = -(f t))
232 (h_f0 : f 0 = 0) (h_f'0 : deriv f 0 = 0) :
233 ∀ t, f t = 0 := by
234 have h_d1 : Differentiable ℝ f := h_diff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
235 have hCD1 : ContDiff ℝ 1 (deriv f) := by
236 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff2
237 rw [contDiff_succ_iff_deriv] at h_diff2; exact h_diff2.2.2
238 have h_dd : Differentiable ℝ (deriv f) := hCD1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
239 -- Energy E(t) = f(t)² + f'(t)² has E' = 2f'(f + f'') = 2f'(f - f) = 0
240 -- So E is constant = E(0) = 0, giving f(t)² ≤ 0, hence f = 0.
241 have hE_deriv_zero : ∀ s, deriv (fun t => f t ^ 2 + deriv f t ^ 2) s = 0 := by
242 intro s
243 have h1 : HasDerivAt (fun x => f x ^ 2 + deriv f x ^ 2)
244 (↑2 * f s ^ (2 - 1) * deriv f s + ↑2 * deriv f s ^ (2 - 1) * deriv (deriv f) s) s :=
245 ((h_d1 s).hasDerivAt.pow 2).add ((h_dd s).hasDerivAt.pow 2)
246 have h2 := h1.deriv; rw [h_ode s] at h2; push_cast at h2; simp only [pow_one] at h2
247 linarith
248 have hE_eq := is_const_of_deriv_eq_zero
249 (show Differentiable ℝ (fun t => f t ^ 2 + deriv f t ^ 2) from
250 (h_d1.pow 2).add (h_dd.pow 2))
251 hE_deriv_zero
252 intro t
253 have hE0 : f 0 ^ 2 + deriv f 0 ^ 2 = 0 := by rw [h_f0, h_f'0]; ring
254 have hEt := hE_eq t 0; simp only [hE0] at hEt
255 nlinarith [sq_nonneg (f t), sq_nonneg (deriv f t)]
256
257private theorem ode_cos_uniqueness (f : ℝ → ℝ)
258 (h_diff : ContDiff ℝ 2 f)
259 (h_ode : ∀ t, deriv (deriv f) t = -(f t))
260 (h_f0 : f 0 = 1) (h_f'0 : deriv f 0 = 0) :
261 ∀ t, f t = Real.cos t := by
262 let g := fun t => f t - Real.cos t
263 have hg_diff : ContDiff ℝ 2 g := h_diff.sub Real.contDiff_cos
264 have hDf : Differentiable ℝ f :=
265 h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
266 have hg_ode : ∀ t, deriv (deriv g) t = -(g t) := by
267 intro t
268 have h1 : deriv g = fun s => deriv f s - deriv Real.cos s :=
269 funext fun s => deriv_sub hDf.differentiableAt Real.differentiable_cos.differentiableAt
270 have hDf1 : ContDiff ℝ 1 (deriv f) := by
271 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff
272 exact (contDiff_succ_iff_deriv.mp h_diff).2.2
273 have hDcos1 : ContDiff ℝ 1 (deriv Real.cos) := by
274 rw [Real.deriv_cos']; exact Real.contDiff_sin.neg
275 have h2 : deriv (deriv g) t = deriv (deriv f) t - deriv (deriv Real.cos) t := by
276 rw [h1]; exact deriv_sub
277 (hDf1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
278 (hDcos1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
279 rw [h2, h_ode t]
280 have : deriv (deriv Real.cos) t = -(Real.cos t) := by
281 have h_dcos : deriv Real.cos = fun x => -Real.sin x := Real.deriv_cos'
282 rw [h_dcos]; exact (Real.hasDerivAt_sin t).neg.deriv
283 rw [this]; ring
284 have hg0 : g 0 = 0 := by simp [g, h_f0, Real.cos_zero]
285 have hg'0 : deriv g 0 = 0 := by
286 have : deriv g 0 = deriv f 0 - deriv Real.cos 0 :=
287 deriv_sub hDf.differentiableAt Real.differentiable_cos.differentiableAt
288 rw [this, h_f'0, Real.deriv_cos, Real.sin_zero, neg_zero, sub_zero]
289 intro t; linarith [ode_neg_zero_uniqueness g hg_diff hg_ode hg0 hg'0 t]
290
291/-- **Aczél–Kannappan classification of the d'Alembert functional equation.**
292
293Any continuous H : ℝ → ℝ with H(0) = 1 satisfying
294 H(t+u) + H(t−u) = 2·H(t)·H(u)
295is exactly one of:
296* the constant 1,
297* `Real.cosh (α·)` for some α ∈ ℝ, or
298* `Real.cos (α·)` for some α ∈ ℝ.
299
300Proof: continuity ⇒ C^∞ via the integration bootstrap (`dAlembert_contDiff_smooth`);
301C² + d'Alembert ⇒ H'' = c·H with c = H''(0) (`dAlembert_to_ODE_general`);
302ODE uniqueness in each branch of the trichotomy on c gives the explicit formula. -/
303theorem dAlembert_classification (H : ℝ → ℝ)
304 (h_one : H 0 = 1) (h_cont : Continuous H)
305 (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
306 (∀ x, H x = 1) ∨
307 (∃ α : ℝ, ∀ x, H x = Real.cosh (α * x)) ∨
308 (∃ α : ℝ, ∀ x, H x = Real.cos (α * x)) := by
309 have h_sm : ContDiff ℝ smooth H := dAlembert_contDiff_smooth H h_one h_cont h_dAl
310 have h2 : ContDiff ℝ 2 H := by exact_mod_cast (contDiff_infty.mp h_sm) 2
311 have hDiff : Differentiable ℝ H := h2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
312 have h_H'0 : deriv H 0 = 0 :=
313 even_deriv_at_zero H (dAlembert_even H h_one h_dAl) hDiff.differentiableAt
314 have h_ode := dAlembert_to_ODE_general H h_sm h_dAl
315 set c := deriv (deriv H) 0 with hc_def
316 have hDD : Differentiable ℝ (deriv H) := by
317 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h2
318 exact (contDiff_succ_iff_deriv.mp h2).2.2.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
319 by_cases hc_pos : 0 < c
320 · -- c > 0: H = cosh(√c · t)
321 right; left; refine ⟨Real.sqrt c, ?_⟩
322 have hsc_ne : Real.sqrt c ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hc_pos)
323 let g : ℝ → ℝ := fun s => H (s / Real.sqrt c)
324 have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c) (Real.sqrt c)⁻¹ s := fun s => by
325 have := (hasDerivAt_id s).div_const (Real.sqrt c); simp only [id, one_div] at this; exact this
326 have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹) s :=
327 fun s => (hDiff _).hasDerivAt.comp s (h_div s)
328 have hg_ode : ∀ t, deriv (deriv g) t = g t := by
329 intro s
330 have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ :=
331 funext fun s => (hg_d s).deriv
332 have h_dd_g : HasDerivAt (deriv g)
333 ((deriv (deriv H) (s / Real.sqrt c) * (Real.sqrt c)⁻¹) * (Real.sqrt c)⁻¹) s := by
334 rw [hg1]
335 exact ((hDD (s / Real.sqrt c)).hasDerivAt.comp s (h_div s)).mul_const _
336 rw [h_dd_g.deriv, h_ode (s / Real.sqrt c)]
337 simp only [g]
338 rw [show c * H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹ =
339 H (s / Real.sqrt c) * (c * ((Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹)) from by ring,
340 show (Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹ = (Real.sqrt c * Real.sqrt c)⁻¹ from
341 (mul_inv_rev _ _).symm,
342 Real.mul_self_sqrt (le_of_lt hc_pos),
343 mul_inv_cancel₀ (ne_of_gt hc_pos), mul_one]
344 intro t
345 have := ode_cosh_uniqueness_contdiff g (h2.comp (contDiff_id.div_const _))
346 hg_ode (by simp [g, h_one]) (by rw [(hg_d 0).deriv]; simp [h_H'0])
347 (Real.sqrt c * t)
348 simp only [g, mul_div_cancel_left₀ _ hsc_ne] at this; exact this
349 · by_cases hc_neg : c < 0
350 · -- c < 0: H = cos(√(−c) · t)
351 right; right; refine ⟨Real.sqrt (-c), ?_⟩
352 set c' := -c
353 have hsc_ne : Real.sqrt c' ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr (neg_pos.mpr hc_neg))
354 let g : ℝ → ℝ := fun s => H (s / Real.sqrt c')
355 have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c') (Real.sqrt c')⁻¹ s := fun s => by
356 have := (hasDerivAt_id s).div_const (Real.sqrt c'); simp only [id, one_div] at this; exact this
357 have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c') * (Real.sqrt c')⁻¹) s :=
358 fun s => (hDiff _).hasDerivAt.comp s (h_div s)
359 have hg_ode : ∀ t, deriv (deriv g) t = -(g t) := by
360 intro s
361 have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c') * (Real.sqrt c')⁻¹ :=
362 funext fun s => (hg_d s).deriv
363 have h_dd_g : HasDerivAt (deriv g)
364 ((deriv (deriv H) (s / Real.sqrt c') * (Real.sqrt c')⁻¹) * (Real.sqrt c')⁻¹) s := by
365 rw [hg1]
366 exact ((hDD (s / Real.sqrt c')).hasDerivAt.comp s (h_div s)).mul_const _
367 rw [h_dd_g.deriv, h_ode (s / Real.sqrt c')]
368 simp only [g, c']
369 rw [show c * H (s / Real.sqrt (-c)) * (Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹ =
370 H (s / Real.sqrt (-c)) * (c * ((Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹)) from by ring,
371 show (Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹ = (Real.sqrt (-c) * Real.sqrt (-c))⁻¹ from
372 (mul_inv_rev _ _).symm,
373 Real.mul_self_sqrt (le_of_lt (neg_pos.mpr hc_neg)),
374 show c * (-c)⁻¹ = -(1 : ℝ) from by
375 have hc_ne : c ≠ 0 := ne_of_lt hc_neg
376 field_simp]
377 ring
378 intro t
379 have := ode_cos_uniqueness g (h2.comp (contDiff_id.div_const _))
380 hg_ode (by simp [g, h_one]) (by rw [(hg_d 0).deriv]; simp [h_H'0])
381 (Real.sqrt c' * t)
382 simp only [g, mul_div_cancel_left₀ _ hsc_ne] at this; exact this
383 · -- c = 0: H ≡ 1
384 left
385 have hc0 : c = 0 := le_antisymm (not_lt.mp hc_pos) (not_lt.mp hc_neg)
386 have h_H'_zero : ∀ t, deriv H t = 0 := by
387 have := is_const_of_deriv_eq_zero hDD (fun t => by rw [h_ode t, hc0, zero_mul])
388 intro t; have := this t 0; simp [h_H'0] at this; exact this
389 intro t
390 have := is_const_of_deriv_eq_zero hDiff h_H'_zero t 0
391 simp [h_one] at this; exact this
392
393private theorem dAlembert_contDiff_top (H : ℝ → ℝ)
394 (h_one : H 0 = 1) (h_cont : Continuous H)
395 (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
396 ContDiff ℝ ⊤ H := by
397 rcases dAlembert_classification H h_one h_cont h_dAl with h | ⟨α, h⟩ | ⟨α, h⟩
398 · rw [show H = fun _ => (1 : ℝ) from funext h]
399 exact contDiff_const
400 · rw [show H = fun t => Real.cosh (α * t) from funext h]
401 exact Real.contDiff_cosh.comp (contDiff_const.mul contDiff_id)
402 · rw [show H = fun t => Real.cos (α * t) from funext h]
403 exact Real.contDiff_cos.comp (contDiff_const.mul contDiff_id)
404
405/-! ## Instance -/
406
407instance : AczelSmoothnessPackage where
408 smooth_of_dAlembert H h_one h_cont h_dAl := dAlembert_contDiff_top H h_one h_cont h_dAl
409
410end
411
412end FunctionalEquation
413end Cost
414end IndisputableMonolith
415