ComponentPotential

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

A zero-trace potential for one affine component correction

This file packages the explicitly zero-extended finite Kuhn interpolation of competitorVertexData C p - linearFn p. On the open root cube it is exactly globalCompetitor m s C p - linearFn p; outside the component's common coarse mesh it vanishes. The resulting compactly supported H¹ function implements the component slope correction as an H¹₀ potential field locally.

noncomputable def Algsuperdiff.Section3.Provider.Affine.componentCorrectionDatum {d : ℕ} (C : Set (HCPolySupport.TriadicCube d)) (p : HCPolySupport.Vec d) : HCPolySupport.Vec d → ℝ

The vertex datum for the scalar correction ℓ̂_p - ℓ_p.

Equations

• Algsuperdiff.Section3.Provider.Affine.componentCorrectionDatum C p x = Algsuperdiff.Section3.Provider.Affine.competitorVertexData C p x - Algsuperdiff.Section3.Provider.Affine.linearFn p x

noncomputable def Algsuperdiff.Section3.Provider.Affine.componentCorrectionPotential {d : ℕ} (m s : ℤ) (C : Set (HCPolySupport.TriadicCube d)) (p : HCPolySupport.Vec d) : HCPolySupport.Vec d → ℝ

The scalar component correction, using the root mesh on the open root and the literal zero representative away from that finite mesh.

Equations

• One or more equations did not get rendered due to their size.

def Algsuperdiff.Section3.Provider.Affine.commonCoarseMeshClosedCarrier {d : ℕ} (N : Finset (HCPolySupport.TriadicCube d)) (s : ℤ) : Set (HCPolySupport.Vec d)

The finite closed-cell carrier of the part of the common coarse mesh subordinate to a component neighborhood.

Equations

• Algsuperdiff.Section3.Provider.Affine.commonCoarseMeshClosedCarrier N s = ⋃ T ∈ ↑(Algsuperdiff.Section3.Provider.Affine.commonCoarseMesh N s), T.closedCarrier

theorem Algsuperdiff.Section3.Provider.Affine.componentCorrectionPotential_eqOn_globalCompetitor_sub_linearFn_closedCarrier {d : ℕ} {m s : ℤ} (hsm : s ≤ m) (C : Set (HCPolySupport.TriadicCube d)) (p : HCPolySupport.Vec d) {T : Whitney.KuhnCell d} (hT : T ∈ rootCoarseMesh m s) : Set.EqOn (componentCorrectionPotential m s C p) (fun (x : HCPolySupport.Vec d) => globalCompetitor m s C p x - linearFn p x) T.closedCarrier

On a closed root-mesh cell, the explicit zero extension is the difference between the global competitor and the linear function.

theorem Algsuperdiff.Section3.Provider.Affine.componentCorrectionPotential_eqOn_globalCompetitor_sub_linearFn {d : ℕ} {m s : ℤ} (hsm : s ≤ m) (C : Set (HCPolySupport.TriadicCube d)) (p : HCPolySupport.Vec d) : Set.EqOn (componentCorrectionPotential m s C p) (fun (x : HCPolySupport.Vec d) => globalCompetitor m s C p x - linearFn p x) (HCPolySupport.cubeSet (HCPolySupport.originCube d m))

On the root cube, the component potential is the raw scalar correction.

theorem Algsuperdiff.Section3.Provider.Affine.closedBall_supportCube_subset_closedBall_of_mem_descendantsAtScale {d : ℕ} {Q R : HCPolySupport.TriadicCube d} {s : ℤ} (hR : R ∈ HCPolySupport.descendantsAtScale Q s) : Metric.closedBall (HCPolySupport.cubeCenter R) (HCPolySupport.cubeRadius R) ⊆ Metric.closedBall (HCPolySupport.cubeCenter Q) (HCPolySupport.cubeRadius Q)

Closed balls of scale descendants are contained in the ancestor's closed ball.

theorem Algsuperdiff.Section3.Provider.Affine.isCompact_commonCoarseMeshClosedCarrier {d : ℕ} (N : Finset (HCPolySupport.TriadicCube d)) (s : ℤ) : IsCompact (commonCoarseMeshClosedCarrier N s)

The common-mesh closed carrier is compact.

theorem Algsuperdiff.Section3.Provider.Affine.commonCoarseMeshClosedCarrier_subset_openCubeSet {d : ℕ} {m s : ℤ} {hn : ℕ → ℕ} {N : Finset (HCPolySupport.TriadicCube d)} (hNsub : ∀ Q ∈ N, Q ∈ Whitney.whitneyPartition m hn) : commonCoarseMeshClosedCarrier N s ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

If every window cube belongs to the Whitney partition, the common-mesh closed carrier lies strictly inside the open root cube.

theorem Algsuperdiff.Section3.Provider.Affine.componentCorrectionPotential_eq_zero_of_notMem_commonCoarseMeshClosedCarrier {d : ℕ} [NeZero d] {m s : ℤ} (hsm : s ≤ m) {hn : ℕ → ℕ} {C : Set (HCPolySupport.TriadicCube d)} (hC : C ⊆ Whitney.whitneyPartition m hn) {N : Finset (HCPolySupport.TriadicCube d)} (hN : ∀ Q ∈ Whitney.whitneyPartition m hn, (∃ R ∈ C, Whitney.CubeTouch Q R) → Q ∈ N) (hs : ∀ Q ∈ N, s ≤ Q.scale) (p : HCPolySupport.Vec d) {x : HCPolySupport.Vec d} (hx : x ∉ commonCoarseMeshClosedCarrier N s) : componentCorrectionPotential m s C p x = 0

The correction potential vanishes away from the finite common-mesh carrier. Root cells omitted from the common mesh carry exactly the linear vertex datum, so their scalar correction is zero.

theorem Algsuperdiff.Section3.Provider.Affine.continuous_componentCorrectionPotential {d : ℕ} [NeZero d] {m s : ℤ} (hsm : s ≤ m) {hn : ℕ → ℕ} {C : Set (HCPolySupport.TriadicCube d)} (hC : C ⊆ Whitney.whitneyPartition m hn) {N : Finset (HCPolySupport.TriadicCube d)} (hNsub : ∀ Q ∈ N, Q ∈ Whitney.whitneyPartition m hn) (hN : ∀ Q ∈ Whitney.whitneyPartition m hn, (∃ R ∈ C, Whitney.CubeTouch Q R) → Q ∈ N) (hs : ∀ Q ∈ N, s ≤ Q.scale) (p : HCPolySupport.Vec d) : Continuous (componentCorrectionPotential m s C p)

The component correction is continuous as an ambient function. On the open root it is the continuous global correction; away from the compact common-mesh carrier it is locally zero.

theorem Algsuperdiff.Section3.Provider.Affine.hasCompactSupport_componentCorrectionPotential {d : ℕ} [NeZero d] {m s : ℤ} (hsm : s ≤ m) {hn : ℕ → ℕ} {C : Set (HCPolySupport.TriadicCube d)} (hC : C ⊆ Whitney.whitneyPartition m hn) {N : Finset (HCPolySupport.TriadicCube d)} (hN : ∀ Q ∈ Whitney.whitneyPartition m hn, (∃ R ∈ C, Whitney.CubeTouch Q R) → Q ∈ N) (hs : ∀ Q ∈ N, s ≤ Q.scale) (p : HCPolySupport.Vec d) : HasCompactSupport (componentCorrectionPotential m s C p)

One component correction has compact support as an ambient function.

theorem Algsuperdiff.Section3.Provider.Affine.memL2_componentCorrectionPotential {d : ℕ} [NeZero d] {m s : ℤ} (hsm : s ≤ m) {hn : ℕ → ℕ} {C : Set (HCPolySupport.TriadicCube d)} (hC : C ⊆ Whitney.whitneyPartition m hn) {N : Finset (HCPolySupport.TriadicCube d)} (hNsub : ∀ Q ∈ N, Q ∈ Whitney.whitneyPartition m hn) (hN : ∀ Q ∈ Whitney.whitneyPartition m hn, (∃ R ∈ C, Whitney.CubeTouch Q R) → Q ∈ N) (hs : ∀ Q ∈ N, s ≤ Q.scale) (p : HCPolySupport.Vec d) : MeasureTheory.MemLp (componentCorrectionPotential m s C p) 2 MeasureTheory.volume

The scalar correction is square-integrable in ambient space.

noncomputable def Algsuperdiff.Section3.Provider.Affine.componentCorrectionWeakGradient {d : ℕ} [NeZero d] (m s : ℤ) (C : Set (HCPolySupport.TriadicCube d)) (p : HCPolySupport.Vec d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The coordinatewise weak-gradient representative for one zero-extended component correction.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Affine.componentCorrectionH1Function {d : ℕ} [NeZero d] {m s : ℤ} (hsm : s ≤ m) {hn : ℕ → ℕ} {C : Set (HCPolySupport.TriadicCube d)} (hC : C ⊆ Whitney.whitneyPartition m hn) {N : Finset (HCPolySupport.TriadicCube d)} (hNsub : ∀ Q ∈ N, Q ∈ Whitney.whitneyPartition m hn) (hN : ∀ Q ∈ Whitney.whitneyPartition m hn, (∃ R ∈ C, Whitney.CubeTouch Q R) → Q ∈ N) (hs : ∀ Q ∈ N, s ≤ Q.scale) (p : HCPolySupport.Vec d) : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))

The canonical H¹ realization of one finite component correction.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algsuperdiff.Section3.Provider.Affine.componentCorrectionH1Function_toFun {d : ℕ} [NeZero d] {m s : ℤ} (hsm : s ≤ m) {hn : ℕ → ℕ} {C : Set (HCPolySupport.TriadicCube d)} (hC : C ⊆ Whitney.whitneyPartition m hn) {N : Finset (HCPolySupport.TriadicCube d)} (hNsub : ∀ Q ∈ N, Q ∈ Whitney.whitneyPartition m hn) (hN : ∀ Q ∈ Whitney.whitneyPartition m hn, (∃ R ∈ C, Whitney.CubeTouch Q R) → Q ∈ N) (hs : ∀ Q ∈ N, s ≤ Q.scale) (p : HCPolySupport.Vec d) : (componentCorrectionH1Function hsm hC hNsub hN hs p).toFun = componentCorrectionPotential m s C p

@[simp]

theorem Algsuperdiff.Section3.Provider.Affine.componentCorrectionH1Function_grad {d : ℕ} [NeZero d] {m s : ℤ} (hsm : s ≤ m) {hn : ℕ → ℕ} {C : Set (HCPolySupport.TriadicCube d)} (hC : C ⊆ Whitney.whitneyPartition m hn) {N : Finset (HCPolySupport.TriadicCube d)} (hNsub : ∀ Q ∈ N, Q ∈ Whitney.whitneyPartition m hn) (hN : ∀ Q ∈ Whitney.whitneyPartition m hn, (∃ R ∈ C, Whitney.CubeTouch Q R) → Q ∈ N) (hs : ∀ Q ∈ N, s ≤ Q.scale) (p : HCPolySupport.Vec d) : (componentCorrectionH1Function hsm hC hNsub hN hs p).grad = componentCorrectionWeakGradient m s C p

theorem Algsuperdiff.Section3.Provider.Affine.memH10_componentCorrectionPotential {d : ℕ} [NeZero d] {m s : ℤ} (hsm : s ≤ m) {hn : ℕ → ℕ} {C : Set (HCPolySupport.TriadicCube d)} (hC : C ⊆ Whitney.whitneyPartition m hn) {N : Finset (HCPolySupport.TriadicCube d)} (hNsub : ∀ Q ∈ N, Q ∈ Whitney.whitneyPartition m hn) (hN : ∀ Q ∈ Whitney.whitneyPartition m hn, (∃ R ∈ C, Whitney.CubeTouch Q R) → Q ∈ N) (hs : ∀ Q ∈ N, s ≤ Q.scale) (p : HCPolySupport.Vec d) : HCPolySupport.MemH10 (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (componentCorrectionPotential m s C p)

Compact support inside the open root upgrades the component correction to H¹₀.

Identification with the component slope field

theorem Algsuperdiff.Section3.Provider.Affine.volume_openCubeSet_diff_iUnion_openCarrier_rootCoarseMesh {d : ℕ} {m s : ℤ} (hsm : s ≤ m) : MeasureTheory.volume (HCPolySupport.openCubeSet (HCPolySupport.originCube d m) \ ⋃ T ∈ ↑(rootCoarseMesh m s), T.openCarrier) = 0

The open cells of a uniform root mesh cover the open root cube up to a Lebesgue-null set.

theorem Algsuperdiff.Section3.Provider.Affine.componentCorrectionWeakGradient_eq_globalCompetitorSlope_sub {d : ℕ} [NeZero d] {m s : ℤ} (hsm : s ≤ m) (C : Set (HCPolySupport.TriadicCube d)) (p : HCPolySupport.Vec d) {x : HCPolySupport.Vec d} (hx : x ∈ ⋃ T ∈ ↑(rootCoarseMesh m s), T.openCarrier) : componentCorrectionWeakGradient m s C p x = globalCompetitorSlope m s C p x - p

On every open root-mesh cell, the weak-gradient representative is exactly the component slope correction ∇ℓ̂_p - p.

theorem Algsuperdiff.Section3.Provider.Affine.componentCorrectionWeakGradient_ae_eq_globalCompetitorSlope_sub {d : ℕ} [NeZero d] {m s : ℤ} (hsm : s ≤ m) (C : Set (HCPolySupport.TriadicCube d)) (p : HCPolySupport.Vec d) : componentCorrectionWeakGradient m s C p =ᵐ[MeasureTheory.volume.restrict (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))] fun (x : HCPolySupport.Vec d) => globalCompetitorSlope m s C p x - p

The weak-gradient representative agrees almost everywhere on the open root with the existing piecewise-constant component slope correction.

theorem Algsuperdiff.Section3.Provider.Affine.isPotentialZeroTraceOn_componentCorrectionWeakGradient {d : ℕ} [NeZero d] {m s : ℤ} (hsm : s ≤ m) {hn : ℕ → ℕ} {C : Set (HCPolySupport.TriadicCube d)} (hC : C ⊆ Whitney.whitneyPartition m hn) {N : Finset (HCPolySupport.TriadicCube d)} (hNsub : ∀ Q ∈ N, Q ∈ Whitney.whitneyPartition m hn) (hN : ∀ Q ∈ Whitney.whitneyPartition m hn, (∃ R ∈ C, Whitney.CubeTouch Q R) → Q ∈ N) (hs : ∀ Q ∈ N, s ≤ Q.scale) (p : HCPolySupport.Vec d) : HCPolySupport.IsPotentialZeroTraceOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (componentCorrectionWeakGradient m s C p)

The canonical weak-gradient representative is an internal zero-trace potential field.

theorem Algsuperdiff.Section3.Provider.Affine.isPotentialZeroTraceOn_globalCompetitorSlope_sub {d : ℕ} [NeZero d] {m s : ℤ} (hsm : s ≤ m) {hn : ℕ → ℕ} {C : Set (HCPolySupport.TriadicCube d)} (hC : C ⊆ Whitney.whitneyPartition m hn) {N : Finset (HCPolySupport.TriadicCube d)} (hNsub : ∀ Q ∈ N, Q ∈ Whitney.whitneyPartition m hn) (hN : ∀ Q ∈ Whitney.whitneyPartition m hn, (∃ R ∈ C, Whitney.CubeTouch Q R) → Q ∈ N) (hs : ∀ Q ∈ N, s ≤ Q.scale) (p : HCPolySupport.Vec d) : HCPolySupport.IsPotentialZeroTraceOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (x : HCPolySupport.Vec d) => globalCompetitorSlope m s C p x - p

The existing component slope correction is an internal zero-trace potential field.

theorem Algsuperdiff.Section3.Provider.Affine.potentialZeroTraceFieldOn_globalCompetitorSlope_sub {d : ℕ} [NeZero d] {m s : ℤ} (hsm : s ≤ m) {hn : ℕ → ℕ} {C : Set (HCPolySupport.TriadicCube d)} (hC : C ⊆ Whitney.whitneyPartition m hn) {N : Finset (HCPolySupport.TriadicCube d)} (hNsub : ∀ Q ∈ N, Q ∈ Whitney.whitneyPartition m hn) (hN : ∀ Q ∈ Whitney.whitneyPartition m hn, (∃ R ∈ C, Whitney.CubeTouch Q R) → Q ∈ N) (hs : ∀ Q ∈ N, s ≤ Q.scale) (p : HCPolySupport.Vec d) : HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (x : HCPolySupport.Vec d) => globalCompetitorSlope m s C p x - p

Public Chapter 1 packaging of the component zero-trace potential field.