Continuity

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Local uniform convergence and continuity of the stream matrix

On the carrier both halves of the scale decomposition converge uniformly on every origin cube: the descending half is exactly the lower-infinite cutoff k_ℓ, already continuous, and the ascending half is dominated on □_ℓ by the summable series Σ_{n > ℓ} d ‖∇j_n‖_{L^∞(□_ℓ)} · 3^{ℓ}/2 produced by the mean value inequality. The normalized field is therefore continuous, and so defines a regular coefficient field in the ambient sense.

Main results

• continuous_streamField — the field is continuous.
• streamRegField — the field as a regular coefficient field.

References

• ABK26, the stream matrix and the scale decomposition.

theorem Algsuperdiff.Section5.Field.continuous_streamField_entry {d : ℕ} {gamma : ℝ} (omega : FullSample d gamma) (i k : Fin d) : Continuous fun (x : HCPolySupport.Vec d) => streamField omega x i k

Continuity of the normalized field, entrywise.

theorem Algsuperdiff.Section5.Field.continuous_streamField {d : ℕ} {gamma : ℝ} (omega : FullSample d gamma) : Continuous (streamField omega)

Continuity of the normalized field.

theorem Algsuperdiff.Section5.Field.symmPart_nu_add_streamField {d : ℕ} {gamma : ℝ} (nu : ℝ) (omega : FullSample d gamma) (x : HCPolySupport.Vec d) : HCPolySupport.symmPart (nu • 1 + streamField omega x) = nu • 1

The symmetric part of ν I + k is exactly ν I, so the normalized field contributes no symmetric part to the coefficient field.