SectorReflectionGeometry

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

Euclidean ball sectors and their partial reflections

This file supplies the finite-face geometry needed to reuse the Section 4 odd-reflection machinery on a Euclidean ball. A finite set S records the coordinate hyperplanes through the centre x₀; sigma i = 1 selects the lower half-space and sigma i = -1 the upper half-space. The intermediate domain partialReflectedBallSector x₀ r S sigma T retains precisely the face constraints in S \ T. It is the original sector at T = ∅ and the full Euclidean ball at T = S.

The finite coordinate-reflection group

def Algsuperdiff.StochasticProcess.Common.Regularity.sectorReflection {d : ℕ} (x₀ : HCPolySupport.Vec d) (J : Finset (Fin d)) : HCPolySupport.Vec d → HCPolySupport.Vec d

Reflection in precisely the coordinate hyperplanes indexed by J, all of which pass through x₀.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.sectorReflection x₀ J y i = if i ∈ J then 2 * x₀ i - y i else y i

def Algsuperdiff.StochasticProcess.Common.Regularity.sectorReflectionLinear {d : ℕ} (J : Finset (Fin d)) : HCPolySupport.Vec d → HCPolySupport.Vec d

The linear action induced on gradients by sectorReflection.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.sectorReflectionLinear J v i = if i ∈ J then -v i else v i

def Algsuperdiff.StochasticProcess.Common.Regularity.sectorReflectionSign {d : ℕ} (J : Finset (Fin d)) : ℝ

The parity sign of a reflection-group element.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.sectorReflectionSign J = (-1) ^ J.card

@[simp]

theorem Algsuperdiff.StochasticProcess.Common.Regularity.sectorReflection_empty {d : ℕ} (x₀ y : HCPolySupport.Vec d) : sectorReflection x₀ ∅ y = y

@[simp]

theorem Algsuperdiff.StochasticProcess.Common.Regularity.sectorReflectionLinear_empty {d : ℕ} (v : HCPolySupport.Vec d) : sectorReflectionLinear ∅ v = v

@[simp]

theorem Algsuperdiff.StochasticProcess.Common.Regularity.sectorReflectionSign_empty {d : ℕ} : sectorReflectionSign ∅ = 1

def Algsuperdiff.StochasticProcess.Common.Regularity.partialReflectedBallSector {d : ℕ} (x₀ : HCPolySupport.Vec d) (r : ℝ) (S : Finset (Fin d)) (sigma : Fin d → ℝ) (T : Finset (Fin d)) : Set (HCPolySupport.Vec d)

The ball sector obtained by retaining the face constraints in S \ T.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.partialReflectedBallSector x₀ r S sigma T = HCPolySupport.euclideanBall x₀ r ∩ ⋂ i ∈ S \ T, {y : HCPolySupport.Vec d | 0 < sigma i * (x₀ i - y i)}

def Algsuperdiff.StochasticProcess.Common.Regularity.ballSector {d : ℕ} (x₀ : HCPolySupport.Vec d) (r : ℝ) (S : Finset (Fin d)) (sigma : Fin d → ℝ) : Set (HCPolySupport.Vec d)

The unreflected Euclidean ball sector.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.ballSector x₀ r S sigma = Algsuperdiff.StochasticProcess.Common.Regularity.partialReflectedBallSector x₀ r S sigma ∅

theorem Algsuperdiff.StochasticProcess.Common.Regularity.mem_partialReflectedBallSector_iff {d : ℕ} {x₀ : HCPolySupport.Vec d} {r : ℝ} {S : Finset (Fin d)} {sigma : Fin d → ℝ} {T : Finset (Fin d)} {y : HCPolySupport.Vec d} : y ∈ partialReflectedBallSector x₀ r S sigma T ↔ y ∈ HCPolySupport.euclideanBall x₀ r ∧ ∀ i ∈ S, i ∉ T → 0 < sigma i * (x₀ i - y i)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.mem_ballSector_iff {d : ℕ} {x₀ : HCPolySupport.Vec d} {r : ℝ} {S : Finset (Fin d)} {sigma : Fin d → ℝ} {y : HCPolySupport.Vec d} : y ∈ ballSector x₀ r S sigma ↔ y ∈ HCPolySupport.euclideanBall x₀ r ∧ ∀ i ∈ S, 0 < sigma i * (x₀ i - y i)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.partialReflectedBallSector_self {d : ℕ} (x₀ : HCPolySupport.Vec d) (r : ℝ) (S : Finset (Fin d)) (sigma : Fin d → ℝ) : partialReflectedBallSector x₀ r S sigma S = HCPolySupport.euclideanBall x₀ r

theorem Algsuperdiff.StochasticProcess.Common.Regularity.partialReflectedBallSector_subset_of_subset {d : ℕ} (x₀ : HCPolySupport.Vec d) (r : ℝ) (S : Finset (Fin d)) (sigma : Fin d → ℝ) {T T' : Finset (Fin d)} (hTT' : T ⊆ T') : partialReflectedBallSector x₀ r S sigma T ⊆ partialReflectedBallSector x₀ r S sigma T'

theorem Algsuperdiff.StochasticProcess.Common.Regularity.ballSector_subset_partialReflectedBallSector {d : ℕ} (x₀ : HCPolySupport.Vec d) (r : ℝ) (S : Finset (Fin d)) (sigma : Fin d → ℝ) (T : Finset (Fin d)) : ballSector x₀ r S sigma ⊆ partialReflectedBallSector x₀ r S sigma T

theorem Algsuperdiff.StochasticProcess.Common.Regularity.isOpen_partialReflectedBallSector {d : ℕ} (x₀ : HCPolySupport.Vec d) (r : ℝ) (S : Finset (Fin d)) (sigma : Fin d → ℝ) (T : Finset (Fin d)) : IsOpen (partialReflectedBallSector x₀ r S sigma T)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.convex_partialReflectedBallSector {d : ℕ} (x₀ : HCPolySupport.Vec d) (r : ℝ) (S : Finset (Fin d)) (sigma : Fin d → ℝ) (T : Finset (Fin d)) : Convex ℝ (partialReflectedBallSector x₀ r S sigma T)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.isBoundedDomain_partialReflectedBallSector {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (S : Finset (Fin d)) (sigma : Fin d → ℝ) (T : Finset (Fin d)) : HCPolySupport.IsBoundedDomain (partialReflectedBallSector x₀ r S sigma T)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.isOpenBoundedConvexDomain_partialReflectedBallSector {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (S : Finset (Fin d)) (sigma : Fin d → ℝ) (T : Finset (Fin d)) : HCPolySupport.IsOpenBoundedConvexDomain (partialReflectedBallSector x₀ r S sigma T)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.euclideanSqDist_coordFaceReflection_center {d : ℕ} (x₀ y : HCPolySupport.Vec d) (i : Fin d) : HCPolySupport.euclideanSqDist (HCPolySupport.coordFaceReflection (x₀ i) i y) x₀ = HCPolySupport.euclideanSqDist y x₀

theorem Algsuperdiff.StochasticProcess.Common.Regularity.mem_euclideanBall_coordFaceReflection_center_iff {d : ℕ} (x₀ : HCPolySupport.Vec d) (r : ℝ) (i : Fin d) (y : HCPolySupport.Vec d) : HCPolySupport.coordFaceReflection (x₀ i) i y ∈ HCPolySupport.euclideanBall x₀ r ↔ y ∈ HCPolySupport.euclideanBall x₀ r

theorem Algsuperdiff.StochasticProcess.Common.Regularity.mem_partialReflectedBallSector_coordFaceReflection_iff {d : ℕ} {x₀ : HCPolySupport.Vec d} {r : ℝ} {S : Finset (Fin d)} {sigma : Fin d → ℝ} {T : Finset (Fin d)} {i : Fin d} (hiT : i ∈ T) (y : HCPolySupport.Vec d) : HCPolySupport.coordFaceReflection (x₀ i) i y ∈ partialReflectedBallSector x₀ r S sigma T ↔ y ∈ partialReflectedBallSector x₀ r S sigma T

Once face i has been unfolded, its intermediate sector is invariant under reflection in that face.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.faceHalf_partialReflectedBallSector_insert {d : ℕ} {x₀ : HCPolySupport.Vec d} {r : ℝ} {S : Finset (Fin d)} {sigma : Fin d → ℝ} {T : Finset (Fin d)} {i : Fin d} (hiS : i ∈ S) (hiT : i ∉ T) : Section4.Provider.ExcessDecay.faceHalf (partialReflectedBallSector x₀ r S sigma (insert i T)) i (x₀ i) (sigma i) = partialReflectedBallSector x₀ r S sigma T

Adding i to the unfolded set removes exactly the i-half-space constraint.