SectorReflectionBox

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

Axis-cube windows as Euclidean ball sectors

This file constructs the face set and signs for a point in the closure of an axis cube. Under the explicit clearance from every face not passing through the point, intersection with a centred Euclidean ball is exactly the canonical ballSector used by the reflection layer.

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.axisCubeFaceSet {d : ℕ} (z : HCPolySupport.Vec d) (L : ℝ) (x₀ : HCPolySupport.Vec d) : Finset (Fin d)

Coordinate faces of axisCube z L which pass through x₀.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.axisCubeFaceSet z L x₀ = {i : Fin d | x₀ i = z i ∨ x₀ i = z i + L}

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.axisCubeFaceOrientation {d : ℕ} (z x₀ : HCPolySupport.Vec d) : Fin d → ℝ

The sign selecting the cube side at a face through x₀: -1 at a lower face and 1 at an upper face.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.axisCubeFaceOrientation z x₀ i = if x₀ i = z i then -1 else 1

theorem Algsuperdiff.StochasticProcess.Common.Regularity.mem_axisCubeFaceSet_iff {d : ℕ} {z : HCPolySupport.Vec d} {L : ℝ} {x₀ : HCPolySupport.Vec d} {i : Fin d} : i ∈ axisCubeFaceSet z L x₀ ↔ x₀ i = z i ∨ x₀ i = z i + L

theorem Algsuperdiff.StochasticProcess.Common.Regularity.abs_axisCubeFaceOrientation {d : ℕ} (z x₀ : HCPolySupport.Vec d) (i : Fin d) : |axisCubeFaceOrientation z x₀ i| = 1

def Algsuperdiff.StochasticProcess.Common.Regularity.MemAxisCubeClosure {d : ℕ} (z : HCPolySupport.Vec d) (L : ℝ) (x₀ : HCPolySupport.Vec d) : Prop

Explicit closure-coordinate data for an axis cube.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.MemAxisCubeClosure z L x₀ = ∀ (i : Fin d), z i ≤ x₀ i ∧ x₀ i ≤ z i + L

def Algsuperdiff.StochasticProcess.Common.Regularity.AxisCubeFaceClearance {d : ℕ} (z : HCPolySupport.Vec d) (L r : ℝ) (x₀ : HCPolySupport.Vec d) : Prop

The ball radius does not reach a lower or upper coordinate face unless that face passes through x₀.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.AxisCubeFaceClearance z L r x₀ = ((∀ (i : Fin d), x₀ i ≠ z i → r ≤ x₀ i - z i) ∧ ∀ (i : Fin d), x₀ i ≠ z i + L → r ≤ z i + L - x₀ i)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.euclideanBall_inter_axisCube_eq_ballSector {d : ℕ} (z : HCPolySupport.Vec d) {L r : ℝ} (hL : 0 < L) (hr : 0 < r) (x₀ : HCPolySupport.Vec d) (hclear : AxisCubeFaceClearance z L r x₀) : HCPolySupport.euclideanBall x₀ r ∩ HCPolySupport.axisCube z L = ballSector x₀ r (axisCubeFaceSet z L x₀) (axisCubeFaceOrientation z x₀)

A ball meeting no unlisted axis-cube face cuts out precisely the sector selected by the faces through its centre.