Source-scale transfer for the corrected transition-window flux.
The two analytic inputs are kept separate: flow distortion controls the
flux-to-gradient time norm, and the previous-scale energy estimate controls
the gradient time norm. The support and exact-flux identities that justify
the first input are proved in R46FluxSupport.
noncomputable def
AVenhance.Infra.Section5.r46TimeL2
(F : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2)
:
The space-time L² norm of the spatial L² norm, in the exact ENNReal
carrier used for the R46 source estimate.
Equations
- AVenhance.Infra.Section5.r46TimeL2 F = (∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal √(AVenhance.gradNormSq (F t)) ^ 2) ^ (1 / 2)