HarmonicGauge

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

Cube/ball gauge transfer for interior harmonic estimates

Vec d = Fin d -> R carries the sup metric, while every interior estimate for a harmonic function is naturally stated on Euclidean balls. CoarseGraining keeps the two gauges separate on the same carrier: openCubeAtScale is the sup-ball and euclideanBall (Sobolev/Foundations/Cutoff/Euclidean) is the explicit round ball defined through vecNormSq. This module proves the two containments relating them, the elementary arithmetic they cost, and the exact volume of a Euclidean ball.

Contents

• sqrt_natCast_le_natCast_add_one_div_two -- the elementary sqrt d <= (d + 1)/2, which is where the dimensional factor of the cube-to-ball direction is paid.
• vecNormSq_sub_center_le_of_mem_openCubeAtScale -- the sharp centred coordinate bound |x - z|^2 <= d (3^m/2)^2 on the cube of scale m.
• openCubeAtScale_subset_euclideanBall -- a cube of scale m sits inside every Euclidean ball of radius > sqrt d * 3^m / 2. This is the direction that costs the sqrt d.
• euclideanClosedBall_subset_openCubeAtScale -- the free direction: a Euclidean closed ball of radius < 3^m / 2 sits inside the cube of scale m.
• volume_euclideanBall_toReal, euclideanUnitBallVolume_pos -- the exact volume r^d omega_d of a Euclidean ball and the positivity of the unit-ball constant omega_d, from which every dimension-only cube-to-ball volume ratio downstream is read off.

The triadic-gap form of the first inclusion --- for a gap k >= d + 2, the Euclidean ball of radius 3^{n+k}/8 around any point of the fine cube z + cu_n stays inside the coarse cube z + cu_{n+k} --- is Corrector.OscillationDecayGap.euclideanBall_eighth_subset_openCubeAtScale_of_gap. That is exactly why the arbitrary-gap oscillation estimate carries the restriction k >= d + 2: a single triadic child need not sit inside the Euclidean ball an interior estimate requires.

References

• ABK26, e.nablaw.oscillations.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.sqrt_natCast_le_natCast_add_one_div_two (d : ℕ) : √↑d ≤ (↑d + 1) / 2

sqrt d <= (d + 1) / 2, the elementary bound 4 d <= (d + 1)^2.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.vecNormSq_sub_center_le_of_mem_openCubeAtScale {d : ℕ} {z : HCPolySupport.Vec d} {m : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.Book.Ch03.openCubeAtScale z m) : HCPolySupport.vecNormSq (x - z) ≤ ↑d * (3 ^ m / 2) ^ 2

The centred coordinate bound.

Every point of the cube z + cu_m is at squared Euclidean distance at most d (3^m / 2)^2 from the centre. This is the sharp constant: the sup-ball of radius 3^m/2 is contained in the Euclidean ball of radius sqrt d * 3^m / 2 and in no smaller one.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.openCubeAtScale_subset_euclideanBall {d : ℕ} {z : HCPolySupport.Vec d} {m : ℤ} {r : ℝ} (hr : √↑d * (3 ^ m / 2) < r) : HCPolySupport.Book.Ch03.openCubeAtScale z m ⊆ HCPolySupport.euclideanBall z r

The expensive direction.

A cube of scale m is contained in every concentric Euclidean ball of radius strictly larger than sqrt d * 3^m / 2.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanClosedBall_subset_openCubeAtScale {d : ℕ} {z : HCPolySupport.Vec d} {m : ℤ} {r : ℝ} (hr0 : 0 ≤ r) (hr : r < 3 ^ m / 2) : HCPolySupport.euclideanClosedBall z r ⊆ HCPolySupport.Book.Ch03.openCubeAtScale z m

The free direction.

A concentric Euclidean closed ball of radius strictly below the half-width 3^m / 2 is contained in the cube of scale m; no dimensional factor is paid because the sup norm never exceeds the Euclidean norm.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.volume_euclideanBall_toReal {d : ℕ} (z : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : (MeasureTheory.volume (HCPolySupport.euclideanBall z r)).toReal = r ^ d * HCPolySupport.Book.Ch01.euclideanUnitBallVolume d

The exact real volume of an explicit Euclidean ball of positive radius.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanUnitBallVolume_pos (d : ℕ) : 0 < HCPolySupport.Book.Ch01.euclideanUnitBallVolume d