TriadicLattice

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

The triadic lattice of centres, and rounding toward the origin

An oscillation estimate produced by a scale-by-scale iteration is available only at lattice centres: at each triadic scale the estimate is proved for the cubes centred at the points of a lattice of that spacing. A Hölder seminorm, by contrast, is a statement about every pair of points. Moving from the one to the other requires replacing an arbitrary centre x by a nearby lattice point z, and the whole cost of that replacement is governed by how far z can be from x.

This file supplies the lattice and the rounding map. Two properties of the rounding are used downstream and both are sharp:

• the displacement is strictly below the lattice spacing, which is what allows the enclosing lattice cube to be exactly one triadic scale up; and
• rounding is done toward the centre of the cube, so |z - c| ≤ |x - c| coordinatewise and the rounded centre never leaves a cube centred at c that contains x.

The second property is what makes the lattice family applicable at the rounded centre: the estimate is available only at lattice points of the cube, and rounding to the nearest lattice point can leave it.

In the ambient space Vec d = Fin d → ℝ the norm is the supremum norm, so a coordinatewise bound on the displacement is a bound on ‖x - z‖.

Main definitions

• triadicLattice s — the set of points of Vec d all of whose coordinates are integer multiples of the spacing s.
• triadicGridPoint s x — the coordinatewise rounding of x toward the origin at spacing s.
• triadicLatticeAt c s, triadicGridPointAt c s x — the same objects for a lattice through an arbitrary base point c, with the rounding done toward c.

Main results

• triadicGridPoint_mem_triadicLattice — the rounded point is a lattice point.
• norm_sub_triadicGridPoint_lt — the displacement is below the spacing.
• norm_triadicGridPoint_le — rounding toward the origin does not increase the norm.
• norm_sub_triadicGridPointAt_lt, triadicGridPointAt_mem_ball — the same two statements for a cube centred at c.

1. Rounding one coordinate toward the origin

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicGridCoord (s t : ℝ) : ℝ

One coordinate of the rounding toward the origin at spacing s: the multiple of s obtained from t by truncating, rather than by rounding to the nearest multiple.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicGridCoord s t = if 0 ≤ t then s * ↑⌊t / s⌋ else s * ↑⌈t / s⌉

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.exists_int_triadicGridCoord (s t : ℝ) : ∃ (n : ℤ), triadicGridCoord s t = s * ↑n

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.abs_sub_triadicGridCoord_lt {s : ℝ} (hs : 0 < s) (t : ℝ) : |t - triadicGridCoord s t| < s

The truncated coordinate is within one spacing of the original, strictly.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.abs_triadicGridCoord_le {s : ℝ} (hs : 0 < s) (t : ℝ) : |triadicGridCoord s t| ≤ |t|

Truncation toward the origin does not increase the absolute value.

2. The lattice and the rounding map

def Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicLattice {d : ℕ} (s : ℝ) : Set (HCPolySupport.Vec d)

The triadic lattice of spacing s: the points of Vec d all of whose coordinates are integer multiples of s. For s = 3 ^ k this is the lattice 3 ^ k ℤ ^ d of the scale-k cubes.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicLattice s = {z : HCPolySupport.Vec d | ∀ (i : Fin d), ∃ (n : ℤ), z i = s * ↑n}

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicGridPoint {d : ℕ} (s : ℝ) (x : HCPolySupport.Vec d) : HCPolySupport.Vec d

Rounding toward the origin at spacing s, coordinate by coordinate.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicGridPoint s x i = Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicGridCoord s (x i)

@[simp]

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicGridPoint_apply {d : ℕ} (s : ℝ) (x : HCPolySupport.Vec d) (i : Fin d) : triadicGridPoint s x i = triadicGridCoord s (x i)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicGridPoint_mem_triadicLattice {d : ℕ} (s : ℝ) (x : HCPolySupport.Vec d) : triadicGridPoint s x ∈ triadicLattice s

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.norm_sub_triadicGridPoint_lt {d : ℕ} {s : ℝ} (hs : 0 < s) (x : HCPolySupport.Vec d) : ‖x - triadicGridPoint s x‖ < s

The displacement of the rounding is below the spacing. Because the ambient norm is the supremum norm, the coordinatewise bound is the bound on the displacement vector.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.norm_triadicGridPoint_le {d : ℕ} {s : ℝ} (hs : 0 < s) (x : HCPolySupport.Vec d) : ‖triadicGridPoint s x‖ ≤ ‖x‖

Rounding toward the origin does not increase the norm.

3. The lattice through an arbitrary base point

def Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicLatticeAt {d : ℕ} (c : HCPolySupport.Vec d) (s : ℝ) : Set (HCPolySupport.Vec d)

The triadic lattice of spacing s through c.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicLatticeAt c s = {z : HCPolySupport.Vec d | z - c ∈ Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicLattice s}

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicGridPointAt {d : ℕ} (c : HCPolySupport.Vec d) (s : ℝ) (x : HCPolySupport.Vec d) : HCPolySupport.Vec d

Rounding toward c at spacing s.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicGridPointAt c s x = c + Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicGridPoint s (x - c)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicGridPointAt_mem_triadicLatticeAt {d : ℕ} (c : HCPolySupport.Vec d) (s : ℝ) (x : HCPolySupport.Vec d) : triadicGridPointAt c s x ∈ triadicLatticeAt c s

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.norm_sub_triadicGridPointAt_lt {d : ℕ} {s : ℝ} (hs : 0 < s) (c x : HCPolySupport.Vec d) : ‖x - triadicGridPointAt c s x‖ < s

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicGridPointAt_mem_ball {d : ℕ} {s rho : ℝ} (hs : 0 < s) {c x : HCPolySupport.Vec d} (hx : x ∈ Metric.ball c rho) : triadicGridPointAt c s x ∈ Metric.ball c rho

Rounding toward the centre keeps the point inside the cube.