refactor: replace d.succ with d (1 of 2)

[zhikaip]

several results were stated over Space d.succ, meaning the parameter d was actually dimension − 1. This is confusing (d should be the dimension) and forces awkward d.succ/d.succ.succ expressions. This PR migrates the Space.Integrals / IsDistBounded lemmas so d is the true dimension.

dimension ≥ 1 → [NeZero d] (typeclass): auto-infers for concrete dims (Space 2/3) contexts
dimension ≥ 2 → (hd : 2 ≤ d := by omega) (autoParam Prop): keeps @[fun_prop] working and auto-discharges at concrete dims contexts. (note: if used with dot notation still requires (by norm_num), but I prefer the clarity)

The distributional-norm results in Space/Norm.lean (distGrad/distDiv/distLaplacian of norm powers and logs, plus the fundamental-solution Laplacian) are still on Space d.succ/.succ.succ/.succ.succ.succ and will migrate in the next PR.

(PR summary partially based on claude code summary but I went through all the changes myself)

Edit: Also remove two duplicate lemmas from mathlib (volume_closedBall_ne_top and volume_closedBall_ne_top)

[github-actions]

Thank you for this PR, which will now be reviewed. Please
see our review guidelines
if you are not familiar with the process. You should expect a back and forth
with a reviewer before your PR is merged. See also that link for how to
add appropriate labels to your PR. The PR will also go through a number
of automated checks. You can learn more about these here,
including how to run them locally.

If you want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

[morrison-daniel]

I think this is a good improvement, just the one question about the two removed lemmas

[morrison-daniel]

Why is this and the next one removed? Are they redundant now?

[zhikaip]

oops I probably should've split this off as they are unrelated to this refactor, but (nevermind I remembered I was checking because they were also stated with d.succ)

basically I found out that they are one-liners with what's already in Mathlib and I don't feel they're necessary, i.e.

lemma volume_closedBall_ne_zero {d : ℕ} (x : Space d.succ) {r : ℝ} (hr : 0 < r) :
    volume (Metric.closedBall x r) ≠ 0 := by
  apply (Metric.measure_closedBall_pos volume _ hr).ne'

lemma volume_closedBall_ne_top {d : ℕ} (x : Space d.succ) (r : ℝ) :
    volume (Metric.closedBall x r) ≠ ⊤ := by
  apply measure_closedBall_lt_top.ne

These only affect the changes in Physlib/ClassicalMechanics/RigidBody/SolidSphere.lean (at the very beginning of the diff page).

[zhikaip]

Updated PR summary to document this change as well

[morrison-daniel]

Ah makes sense!