feat(Space): add radial norm-power divergence formula

[Lemmy00]

This adds a distributional divergence formula for radial norm-power vector fields on Space d.succ.

The main new result is:

lemma Space.distDiv_norm_zpow_smul_repr_self_eq_smul
    {d : ℕ} (q : ℤ) (hq : 0 < q + (d.succ : ℤ)) :
    ∇ᵈ ⬝ (distOfFunction (fun x : Space d.succ => ‖x‖ ^ q • basis.repr x)
      (IsDistBounded.zpow_smul_repr_self q (by omega))) =
      (((q + (d.succ : ℤ) : ℤ) : ℝ) •
        distOfFunction (fun x : Space d.succ => ‖x‖ ^ q)
          (IsDistBounded.pow q (by omega)))

This is intended as the first small PR toward the odd-dimensional Laplacian fundamental-solution/Riesz-kernel identity discussed on Zulip. It generalizes the off-origin radial divergence step used before specializing to the existing distDiv_inv_pow_eq_dim boundary result.

The proof uses spherical coordinates and one-dimensional integration by parts on the radial coordinate.

Checks run locally:

lake update
lake exe cache get
lake build
lake build Physlib.SpaceAndTime.Space.Norm
lake build Physlib
./scripts/lint-style.py Physlib/SpaceAndTime/Space/Norm.lean
git diff --check

I also ran lake exe lint_all; it completed with existing unrelated style/transitive-import reports elsewhere in the repository, while the Lean linter section passed for Physlib.

Prepared with assistance from OpenAI Codex.

P.S.

Planned follow-up PRs, assuming this direction:

1. Add the distributional Laplacian recurrence for norm powers:

   Δᵈ (distOfFunction (fun x : Space d.succ => ‖x‖ ^ a) ...) =
     ((a : ℝ) * (((a - 2) + (d.succ : ℤ) : ℤ) : ℝ)) •
       distOfFunction (fun x : Space d.succ => ‖x‖ ^ (a - 2)) ...

2. Repackage the boundary Riesz step as a Laplacian theorem, using the existing distDiv_inv_pow_eq_dim.

3. Iterate the recurrence in odd dimension 2 * m + 1 to prove the real distributional fundamental-solution statement:

   ∃ c : ℝ, c ≠ 0 ∧
     ((Δᵈ^[m + 1]) (distribution induced by fun x => ‖x‖) =
       c • Physlib.Distribution.diracDelta ℝ 0)

4. Optionally expose the exact dimensional constant if reviewers prefer that over the existential form.

5. Keep the complex tempered-distribution/Fourier bridge downstream for now, unless maintainers think that layer also belongs in Physlib.

[jstoobysmith]

As a quick look at this - my first comment is that, the proofs look kind of long. Is there anyway we can either:

1. Break them down into smaller lemmas, or
2. Golf the proofs to make them shorter?

[Lemmy00]

Thanks, agreed. I pushed a refactor which splits the long proof into smaller private lemmas:

• sphere/radial norm bookkeeping,
• the radial derivative as an inner product with the gradient,
• the two zpow/Jacobian arithmetic steps,
• the spherical-coordinate integral rewrite,
• and the divergence-to-radial-derivative reduction.

The public theorem proof is now mostly the final calc: reduce to the radial derivative integral, apply the one-dimensional integration-by-parts lemma, convert back from spherical coordinates, and identify the scalar multiple of distOfFunction.

I also golfed a couple of the pure algebra blocks. Locally I reran:

lake build Physlib.SpaceAndTime.Space.Norm
lake build Physlib
./scripts/lint-style.py Physlib/SpaceAndTime/Space/Norm.lean
git diff --check

[jstoobysmith]

I think this lemma can be generalized and put in an Integrals file.

[jstoobysmith]

I think this still needs to be done here.

[Lemmy00]

Addressed. I moved radial_norm_power_spherical_integral_eq_space_integral out of Norm.lean into Space/Integrals/NormPow.lean as a public integral lemma, and Norm.lean now imports and reuses it.

Verified with lake build Physlib.SpaceAndTime.Space.Integrals.NormPow, lake build Physlib.SpaceAndTime.Space.Norm, full lake build Physlib, style lint, git diff --check, and a sorry/admit scan on the touched files.

[Lemmy00]

Thanks, addressed.

I checked for reusable results before adding/moving anything:

• Replaced the local radial derivative helper with the existing grad_smul_inner_space from Space/Derivatives/Grad.lean.
• Moved the radial Jacobian zpow algebra lemmas to Space/Integrals/Basic.lean.
• Promoted the scalar spherical integrability statement to IsDistBounded.integrable_space_mul_spherical; I did not find an existing exact scalar version, only the existing inner-gradient spherical integrability lemma.

Verification:

• lake build Physlib.SpaceAndTime.Space.Integrals.Basic
• lake build Physlib.SpaceAndTime.Space.IsDistBounded
• lake build Physlib.SpaceAndTime.Space.Norm
• lake build Physlib
• ./scripts/lint-style.py ...
• git diff --check

[jstoobysmith]

would you mind fixing the merge conflict on this PR. Sorry about this. (I'm also at a workshop currently - so sorry for my slow responses to changes).

[Lemmy00]

would you mind fixing the merge conflict on this PR. Sorry about this. (I'm also at a workshop currently - so sorry for my slow responses to changes).

No worries at all. Done.

[jstoobysmith]

I'm struggling a bit with this PR, so I am going to try and articulate why, but may not do the best job at it:

I think a lot of the lemmas are still in the wrong place, and not in there most obvious general form. For example, it doesn't really make sense for the lemmas like norm_smul_sphere to be in that file alone., and I think radial_norm_power_spherical_integral_eq_space_integral can be generalized to some lemma about general integrals, and spherical integrals which would make it much more useful.

[Lemmy00]

I'm struggling a bit with this PR, so I am going to try and articulate why, but may not do the best job at it:

I think a lot of the lemmas are still in the wrong place, and not in there most obvious general form. For example, it doesn't really make sense for the lemmas like norm_smul_sphere to be in that file alone., and I think radial_norm_power_spherical_integral_eq_space_integral can be generalized to some lemma about general integrals, and spherical integrals which would make it much more useful.

Thanks, I agree this needed a more structural refactor.

I pushed 3a1e178f, which changes the shape of the API rather than only moving the old lemma:

• moved norm_smul_sphere to Space/Module.lean, since it is a general geometric fact about Space;
• added general spherical-coordinate integral lemmas in Space/Integrals/Basic.lean, including an integrability transport lemma and a reusable integral_volume_eq_spherical_integral;
• removed the specialized IsDistBounded.integrable_space_mul_spherical;
• kept the norm-power-specific zpow/Jacobian arithmetic in Space/Integrals/NormPow.lean;
• rewrote radial_norm_power_spherical_integral_eq_space_integral as a short specialization of the new general integral lemma.

Verification:
lake build Physlib.SpaceAndTime.Space.Integrals.NormPow
lake build Physlib.SpaceAndTime.Space.Norm
lake build Physlib
lake exe runPhyslibLinters
focused style lint, git diff upstream/master --check, and a sorry/admit scan on touched files.

[jstoobysmith]

This looks much better. Couple of last things - can we swap the equality present in this lemma.

[jstoobysmith]

This now looks good - many thanks for this PR and going through the review process. I've approved this.