CubeTransport

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

Moving the cube quantities between y + □_m and the origin cube

The oscillation family of the regularity theorem is stated on the origin cube □_m, while the localized estimates are read on the translated cube y + □_m. Lebesgue measure is translation invariant, so the volume average and the volume-normalized L² seminorm move between the two frames with no constant; this file records those two identities, the two elementary volume facts about y + □_m, and the exponent monotonicity of the normalized Hölder seminorm on a cube.

Main results

• volumeAverage_cubeSetAt, normalizedL2On_cubeSetAt — the two transports.
• ofReal_rpow_mul_holderSeminormOn_mono — the normalized seminorm 3 ^ (alpha m) [f]_{C^{0,alpha}(y + □_m)} increases with the exponent, since two points of the cube are less than 3 ^ m apart.
• ofReal_normalizedL2On_le_eLpNorm — the dictionary between the seminorm ‖·‖_{L²(y + □_m)} and the eLpNorm against the normalized volume measure.

1. The cube at the origin, and its volume

theorem Algsuperdiff.Section4.Provider.Holder.cubeSetAt_zero_eq {d : ℕ} (m : ℤ) : Section5.Support.cubeSetAt 0 m = HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

The cube centred at the origin is the origin cube.

theorem Algsuperdiff.Section4.Provider.Holder.volume_cubeSetAt_ne_top {d : ℕ} (y : HCPolySupport.Vec d) (m : ℤ) : MeasureTheory.volume (Section5.Support.cubeSetAt y m) ≠ ⊤

theorem Algsuperdiff.Section4.Provider.Holder.volume_cubeSetAt_pos {d : ℕ} (y : HCPolySupport.Vec d) (m : ℤ) : 0 < MeasureTheory.volume (Section5.Support.cubeSetAt y m)

2. The two transports

theorem Algsuperdiff.Section4.Provider.Holder.volumeAverage_cubeSetAt {d : ℕ} (y : HCPolySupport.Vec d) (m : ℤ) (f : HCPolySupport.Vec d → ℝ) : HCPolySupport.volumeAverage (Section5.Support.cubeSetAt y m) f = HCPolySupport.volumeAverage (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (x : HCPolySupport.Vec d) => f (x + y)

The volume average over y + □_m is the volume average over □_m of the recentred integrand.

theorem Algsuperdiff.Section4.Provider.Holder.normalizedL2On_cubeSetAt {d : ℕ} (y : HCPolySupport.Vec d) (m : ℤ) (f : HCPolySupport.Vec d → ℝ) : Support.normalizedL2On (Section5.Support.cubeSetAt y m) f = Support.normalizedL2On (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (x : HCPolySupport.Vec d) => f (x + y)

The volume-normalized L² seminorm over y + □_m is the seminorm over □_m of the recentred integrand.

3. Exponent monotonicity of the normalized Hölder seminorm

theorem Algsuperdiff.Section4.Provider.Holder.holderSeminormOn_le_rpow_mul {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (y : HCPolySupport.Vec d) (m : ℤ) {alpha beta : ℝ} (hab : alpha ≤ beta) (f : HCPolySupport.Vec d → E) : Section5.Support.holderSeminormOn (Section5.Support.cubeSetAt y m) alpha f ≤ ENNReal.ofReal (Real.rpow 3 ((beta - alpha) * ↑m)) * Section5.Support.holderSeminormOn (Section5.Support.cubeSetAt y m) beta f

The Hölder seminorm on a cube decreases with the exponent, up to the diameter weight. Two points of y + □_m are less than 3 ^ m apart, so a difference quotient at exponent alpha is at most 3 ^ ((beta - alpha) m) times the quotient at the larger exponent beta.

theorem Algsuperdiff.Section4.Provider.Holder.ofReal_rpow_mul_holderSeminormOn_mono {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (y : HCPolySupport.Vec d) (m : ℤ) {alpha beta : ℝ} (hab : alpha ≤ beta) (f : HCPolySupport.Vec d → E) : ENNReal.ofReal (Real.rpow 3 (alpha * ↑m)) * Section5.Support.holderSeminormOn (Section5.Support.cubeSetAt y m) alpha f ≤ ENNReal.ofReal (Real.rpow 3 (beta * ↑m)) * Section5.Support.holderSeminormOn (Section5.Support.cubeSetAt y m) beta f

The normalized seminorm 3 ^ (alpha m) [f]_{C^{0,alpha}(y + □_m)} is monotone in the exponent.

4. The seed dictionary

instance Algsuperdiff.Section4.Provider.Holder.isFiniteMeasure_volume_restrict_cubeSetAt {d : ℕ} (y : HCPolySupport.Vec d) (m : ℤ) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (Section5.Support.cubeSetAt y m))

theorem Algsuperdiff.Section4.Provider.Holder.memLp_sub_volumeAverage_cubeSetAt {d : ℕ} (y : HCPolySupport.Vec d) (m : ℤ) (u : HCPolySupport.H1Function (Section5.Support.cubeSetAt y m)) : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => u.toFun x - HCPolySupport.volumeAverage (Section5.Support.cubeSetAt y m) u.toFun) 2 (MeasureTheory.volume.restrict (Section5.Support.cubeSetAt y m))

The mean-subtracted solution is square integrable on the cube.

theorem Algsuperdiff.Section4.Provider.Holder.ofReal_normalizedL2On_le_eLpNorm {d : ℕ} (y : HCPolySupport.Vec d) (m : ℤ) {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Section5.Support.cubeSetAt y m))) : ENNReal.ofReal (Support.normalizedL2On (Section5.Support.cubeSetAt y m) f) ≤ MeasureTheory.eLpNorm f 2 (Support.normalizedVolumeMeasureOn (Section5.Support.cubeSetAt y m))

The seed dictionary. The volume-normalized L² seminorm on the cube is bounded by the eLpNorm against the normalized volume measure, the form the localized estimate is written in.