BesovCongr #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Almost-everywhere congruence for the positive q = 2 Besov quantities #
The frozen D_h statement speaks about the actual coefficient fields, while
every regularity estimate available for them is proved for a Lipschitz
representative that agrees with the field only almost everywhere. All the
positive Besov quantities are built from cubeLpNorm and cubeAverage, both
integral quantities, so they are insensitive to a.e. modification. This module
records that insensitivity once.
The only nontrivial step is that a.e. equality on a parent cube descends to
every descendant cube, which follows from
normalizedCubeMeasure_descendant_eq_smul_restrict.
The normalized cube measure and the restricted volume have the same #
null sets
An a.e. identity on a parent cube holds a.e. on every descendant cube.