Add analytic structures for WithDim

[catlover-bot]

Motivation

I would like to work on analytic structures for WithDim d M as a separate contribution from #1626.

At 45336685, Physlib/Units/WithDim/Basic.lean already provides additive and order structures, an NNReal action, dimension-changing multiplication/division, and casts. It ends with a TODO for further inherited structures, including topology. It does not yet provide the real-module and normed-space structures needed to use dimension-tagged values directly with the calculus API.

Physlib/Units/FDeriv.lean already proves dimensional correctness of the Fréchet derivative under its stated hypotheses. I would reuse that theory rather than introduce a competing definition of differentiability.

Proposed first PR

Keep the WithDim representation and existing operations, and add a coherent analytic layer:

• Lift the scalar/module structure needed for real analysis, preserving the existing NNReal action and avoiding competing scalar-action instances.
• Transport the normed additive-group and normed-space structures from the underlying value type, with explicit coordinate equivalences and basic projection/construction lemmas. Keep this basis-generic where the existing type is basis-generic.
• Include integration examples using continuity and HasFDerivAt on tagged values, plus regression tests for existing unit rescaling, casts, and rejection of mixed-dimension assignments/addition.

The aim is one usable foundation PR, not a collection of unrelated instance additions. I would reuse Mathlib's transport constructions where suitable, without replacing the existing additive operations with a second incompatible instance hierarchy.

Boundaries

The transported norm is the norm of the chosen numerical representation; it is not claimed to be invariant under a change of units. The first PR would not redesign UnitSystem, generalize the existing LTMCT unit-scaling layer, or introduce a Ring/Field instance on an arbitrary fixed physical dimension.

A scalar derivative tagged by output dimension divided by input dimension, together with position/velocity/acceleration examples, would be a follow-up. Normed-space instances alone do not give an ordinary fderiv that quotient-dimension tag, nor do they make an arbitrary differentiable function dimensionally correct.

Question

Would this be an appropriate first scope for addressing the WithDim TODO? My preference is to keep only necessary algebraic additions in WithDim/Basic.lean and place the analytic layer in a focused adjacent module, subject to the preferred import layout.

[jstoobysmith]

This sounds good to me. I think we should also think about here how we can actually implement this in the real examples that go throughout Physlib. That is, what is the best API that we can build around the units here that will mean that it will transport as well as possible.