From 6b4b89aa1cdfb027789825becbcf8bcf19f72684 Mon Sep 17 00:00:00 2001 From: ZhiKai Pong Date: Tue, 22 Sep 2026 18:57:29 +0100 Subject: [PATCH 1/2] =?UTF-8?q?feat(Space):=20register=20`NormedSpace=20?= =?UTF-8?q?=E2=84=9D=20(Space=20d)`=20as=20a=20direct=20instance?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `Space d` only obtained `NormedSpace ℝ` as the projection `InnerProductSpace.toNormedSpace`, which typeclass search does not find when it arises as a nested subgoal, so instances such as `NormSMulClass ℝ (Space d →L[ℝ] ℝ)` and `ContinuousENorm (Space d →L[ℝ] ℝ)` were unreachable. Registering the same term as a direct instance fixes this; it is defeq at instance transparency to the projection and its module structure is the existing `Space.instModuleReal`. Co-Authored-By: Claude Fable 5.1 --- Physlib/SpaceAndTime/Space/Module.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Physlib/SpaceAndTime/Space/Module.lean b/Physlib/SpaceAndTime/Space/Module.lean index 50117b0ac..9d08b88b5 100644 --- a/Physlib/SpaceAndTime/Space/Module.lean +++ b/Physlib/SpaceAndTime/Space/Module.lean @@ -253,6 +253,14 @@ instance {d} : InnerProductSpace ℝ (Space d) where simpa only [smul_vadd_zero, inner_vadd_zero, conj_trivial] using InnerProductSpace.smul_left v1 v2 a +/-- The normed space structure on `Space d`, registered directly. It is definitionally the + one underlying the inner product space structure, but registering it as its own instance is + needed for typeclass search to find the operator-norm structure on `Space d →L[ℝ] ℝ` + (for example `NormSMulClass ℝ (Space d →L[ℝ] ℝ)`), which is not found when + `NormedSpace ℝ (Space d)` arises only as a nested subgoal through + `InnerProductSpace.toNormedSpace`. -/ +noncomputable instance {d} : NormedSpace ℝ (Space d) := InnerProductSpace.toNormedSpace + lemma norm_smul_sphere {d : ℕ} (n : ↑(Metric.sphere (0 : Space d) 1)) {r : ℝ} (hr : 0 ≤ r) : ‖(r • (n : Space d))‖ = r := by From 1cfbac7f03ea4a1190b7c547baadd236f09d17ce Mon Sep 17 00:00:00 2001 From: ZhiKai Pong Date: Tue, 22 Sep 2026 19:50:36 +0100 Subject: [PATCH 2/2] refactor(SpaceAndTime): remove maxSynthPendingDepth options from schwartzMap_fderiv_integrable_slice_symm and integrable_fderiv_space MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit With the direct `NormedSpace ℝ (Space d)` instance, `Integrable` of `Space d →L[ℝ] ℝ`-valued functions no longer needs a raised `maxSynthPendingDepth`: - `Space/ConstantSliceDist.lean`: `schwartzMap_fderiv_integrable_slice_symm`; - `TimeAndSpace/ConstantTimeDist.lean`: `integrable_fderiv_space`. Co-Authored-By: Claude Opus 5.5 --- Physlib/SpaceAndTime/Space/ConstantSliceDist.lean | 1 - Physlib/SpaceAndTime/TimeAndSpace/ConstantTimeDist.lean | 1 - 2 files changed, 2 deletions(-) diff --git a/Physlib/SpaceAndTime/Space/ConstantSliceDist.lean b/Physlib/SpaceAndTime/Space/ConstantSliceDist.lean index 48b9999f0..7449bfe81 100644 --- a/Physlib/SpaceAndTime/Space/ConstantSliceDist.lean +++ b/Physlib/SpaceAndTime/Space/ConstantSliceDist.lean @@ -171,7 +171,6 @@ lemma schwartzMap_integrable_slice_symm {d : ℕ} (i : Fin d.succ) (η : 𝓢(Sp · fun_prop · simp -set_option maxSynthPendingDepth 10000 in lemma schwartzMap_fderiv_integrable_slice_symm {d : ℕ} (η : 𝓢(Space d.succ, ℝ)) (x : Space d) (i : Fin d.succ) : Integrable (fun r => fderiv ℝ (fun x => η (((slice i).symm (r, x)))) x) volume := by diff --git a/Physlib/SpaceAndTime/TimeAndSpace/ConstantTimeDist.lean b/Physlib/SpaceAndTime/TimeAndSpace/ConstantTimeDist.lean index a0e8f1260..e8e2b0994 100644 --- a/Physlib/SpaceAndTime/TimeAndSpace/ConstantTimeDist.lean +++ b/Physlib/SpaceAndTime/TimeAndSpace/ConstantTimeDist.lean @@ -292,7 +292,6 @@ lemma time_integral_differentiable {d : ℕ} (η : 𝓢(Time × Space d, ℝ)) : -/ -set_option maxSynthPendingDepth 10000 in @[fun_prop] lemma integrable_fderiv_space {d : ℕ} (η : 𝓢(Time × Space d, ℝ)) (x : Space d) : Integrable (fun t => fderiv ℝ (fun x => η (t, x)) x) volume := by