CubeCarrier

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

The translated triadic cube y + □_n

Section 5 localizes its Dirichlet problems on cubes y + □_n whose centre y is an arbitrary point of ℝ^d, not a triadic lattice point. The triadic-cube descriptor TriadicCube d carries an integer index, so y + □_n is not of the form openCubeSet Q; this file introduces the translated carrier as a set and proves the geometric facts the Section 5 solvability and regularity statements consume.

Main definitions

• cubeSetAt y n — the open cube of side 3^n centred at y, realized as the image of openCubeSet (originCube d n) under x ↦ y + x.

Main results

• cubeSetAt_eq_translateSet — the image carrier agrees with the ambient translation operator translateSet, whose Sobolev transport API is available.
• mem_cubeSetAt_iff — membership is membership of the recentred point.
• isOpen_cubeSetAt, measurableSet_cubeSetAt, convex_cubeSetAt, isOpenBoundedConvexDomain_cubeSetAt — the domain hypotheses required by the variational solvability theory.
• mem_cubeSetAt_self — the centre belongs to its own cube, so the carrier is never empty.
• norm_sub_lt_of_mem_cubeSetAt — the diameter bound ‖x - z‖ < 3^n in the ambient supremum norm.

References

• ABK26, the localized Dirichlet problems of Section 5.1.

def Algsuperdiff.Section5.Support.cubeSetAt {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : Set (HCPolySupport.Vec d)

The cube y + □_n: the open triadic cube of side 3^n centred at the origin, translated so that its centre is y.

Equations

• Algsuperdiff.Section5.Support.cubeSetAt y n = (fun (x : HCPolySupport.Vec d) => y + x) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)

theorem Algsuperdiff.Section5.Support.cubeSetAt_zero_eq_openCubeSet {d : ℕ} (n : ℤ) : cubeSetAt 0 n = HCPolySupport.openCubeSet (HCPolySupport.originCube d n)

The translated cube centred at the origin is the origin cube.

theorem Algsuperdiff.Section5.Support.cubeSetAt_eq_translateSet {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : cubeSetAt y n = HCPolySupport.translateSet y (HCPolySupport.openCubeSet (HCPolySupport.originCube d n))

The image realization of y + □_n is the ambient translation of the origin cube; this is the form the Sobolev transport API is stated in.

theorem Algsuperdiff.Section5.Support.mem_cubeSetAt_iff {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {x : HCPolySupport.Vec d} : x ∈ cubeSetAt y n ↔ x - y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d n)

Membership in y + □_n is membership of the recentred point in □_n.

theorem Algsuperdiff.Section5.Support.mem_cubeSetAt_iff_forall_coord {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {x : HCPolySupport.Vec d} : x ∈ cubeSetAt y n ↔ ∀ (i : Fin d), -(1 / 2) * 3 ^ n < x i - y i ∧ x i - y i < 1 / 2 * 3 ^ n

The coordinate description of y + □_n.

theorem Algsuperdiff.Section5.Support.isOpen_cubeSetAt {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : IsOpen (cubeSetAt y n)

theorem Algsuperdiff.Section5.Support.measurableSet_cubeSetAt {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : MeasurableSet (cubeSetAt y n)

theorem Algsuperdiff.Section5.Support.convex_cubeSetAt {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : Convex ℝ (cubeSetAt y n)

theorem Algsuperdiff.Section5.Support.isOpenBoundedConvexDomain_cubeSetAt {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : HCPolySupport.IsOpenBoundedConvexDomain (cubeSetAt y n)

y + □_n is an open bounded convex domain, the hypothesis under which the variational Dirichlet theory is available.

theorem Algsuperdiff.Section5.Support.mem_cubeSetAt_self {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : y ∈ cubeSetAt y n

The centre lies in its own cube; in particular y + □_n is nonempty.

theorem Algsuperdiff.Section5.Support.cubeSetAt_nonempty {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : (cubeSetAt y n).Nonempty

theorem Algsuperdiff.Section5.Support.norm_sub_lt_of_mem_cubeSetAt {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {x z : HCPolySupport.Vec d} (hx : x ∈ cubeSetAt y n) (hz : z ∈ cubeSetAt y n) : ‖x - z‖ < 3 ^ n

Two points of y + □_n are less than 3^n apart in the ambient supremum norm.