L2Bridge

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

The L² carrier bridge of the interior clause

  eLpNorm (fun y => u y - (u)_W) 2 (normalizedVolumeMeasureOn W) ,
      W = ((z + □_{n+2}) ∩ □_m) ,

an ℝ≥0∞ L² norm on the anchor's window.

• the ⨍-square versus the normalized L² norm on an open cube — CoarseGraining's normalizedL2SqOnSet_openCubeSet_eq_cubeLpNorm_two_sq, whose MemLp side condition is discharged here from the H¹ structure itself (H1Function.memL2), not assumed;
• the real translation z, which moves the norm and the subtracted mean together (ForceTransport.lean for the norm, CoarseGraining's volumeAverage_translateSet_eq_comp_addRight for the mean).

Both are equalities: the bridge introduces no constant.

Main results

• memLp_two_normalizedCubeMeasure_of_h1, memLp_two_sub_volumeAverage_of_h1 — the L² data of an H¹ function in the normalized cube measure.
• normalizedL2SqOnSet_sub_average_eq_eLpNorm_sq — the ⨍-square is the square of the normalized L² norm (at the origin cube).

References

• ABK26, l.harmonic.approximation.good.scales, (the ‖u - (u)_W‖_{L²(W)} slot).
• CoarseGraining, Homogenization/Book/Ch03/Theorems/CoarseCaccioppoli/ZeroTraceValue.lean, Homogenization/Book/Ch01/Theorems/NormScaling.lean.

1. The L² data of an H¹ function in the normalized measure

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedCubeMeasure_eq_smul_restrict_openCubeSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) : HCPolySupport.normalizedCubeMeasure Q = ENNReal.ofReal (HCPolySupport.cubeVolume Q)⁻¹ • MeasureTheory.volume.restrict (HCPolySupport.openCubeSet Q)

The normalized cube measure is the volume-normalized restriction to the open cube.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.memLp_two_normalizedCubeMeasure_of_h1 {d : ℕ} (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) : MeasureTheory.MemLp u.toFun 2 (HCPolySupport.normalizedCubeMeasure Q)

An H¹ function on the open cube is L² for the normalized cube measure.

2. The ⨍-square is the normalized L² norm squared

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2SqOnSet_sub_average_eq_eLpNorm_sq_of_memLp {d : ℕ} (Q : HCPolySupport.TriadicCube d) (v : HCPolySupport.Vec d → ℝ) (hv : MeasureTheory.MemLp v 2 (HCPolySupport.normalizedCubeMeasure Q)) : (HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet Q) fun (y : HCPolySupport.Vec d) => v y - HCPolySupport.volumeAverage (HCPolySupport.openCubeSet Q) v) = (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => v y - HCPolySupport.volumeAverage (HCPolySupport.openCubeSet Q) v) 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet Q))).toReal ^ 2

The same for a bare function with an explicit L² datum (the form in which the composed interior estimate consumes it, after the H¹ carrier has been eliminated).

3. The bridge to the anchor's window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2SqOnSet_translate_sub_average_eq_eLpNorm_sq_image_add {d : ℕ} {z : HCPolySupport.Vec d} (Q : HCPolySupport.TriadicCube d) (f : HCPolySupport.Vec d → ℝ) (hf : MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => f (y + z)) 2 (HCPolySupport.normalizedCubeMeasure Q)) : (HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet Q) fun (y : HCPolySupport.Vec d) => f (y + z) - HCPolySupport.volumeAverage (HCPolySupport.openCubeSet Q) fun (x : HCPolySupport.Vec d) => f (x + z)) = (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => f y - HCPolySupport.volumeAverage ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet Q) f) 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet Q))).toReal ^ 2

The L² carrier bridge, in bare-function form.