BoundaryReflectionChain

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

Unfolding a sector weak solution into the full ball

A divergence-form weak solution on a Euclidean ball sector whose values vanish on the flat faces extends oddly, one face at a time, to the whole centred ball. At each unfolding step the coefficient is conjugated by the coordinate sign flip and the scalar source is extended oddly, so the small-contrast bound is preserved and the source only doubles. The chain records the resulting weak equation together with the pointwise oddness and the pinning to the original sector datum.

The same induction over the same sector geometry, with the same four invariants, appears once more for the Laplacian in Regularity/SectorReflectionHarmonic.lean. Harmonicity is the special case a = 1, g = 0 of the equation unfolded here, so the harmonic chain is an instance of this one; it is kept separate only because it additionally exports gradient-level reflection symmetry to the sector energy comparison. Once the sector Campanato route no longer needs that export, the harmonic chain should be re-derived from this one behind a single equivalence between the harmonic predicate and its divergence-form reading.

1. Pointwise algebra of the reflected flux

2. The unfolding chain

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.exists_oddReflection_weakSolution_chain {d : ℕ} {x₀ : HCPolySupport.Vec d} {r : ℝ} (hr : 0 < r) {S : Finset (Fin d)} {sigma : Fin d → ℝ} (hsigma : ∀ i ∈ S, |sigma i| = 1) {a : HCPolySupport.CoeffField d} {delta M : ℝ} (hM : 0 ≤ M) (hameas : Measurable a) (hcontrast : Ported.CoefficientIdentityDistanceLE (ballSector x₀ r S sigma) a delta) (v : HCPolySupport.H1Function (ballSector x₀ r S sigma)) (hzt : HCPolySupport.LocalizedZeroTraceFunctionOn (ballSector x₀ r S sigma) (HCPolySupport.euclideanBall x₀ r) v.toFun) {g : HCPolySupport.Vec d → ℝ} (hgL2 : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (ballSector x₀ r S sigma))) (hgM : ∀ᵐ (y : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (ballSector x₀ r S sigma), |g y| ≤ M) (hflux : ∀ (j : Fin d), MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => HCPolySupport.matVecMul (a y) (v.grad y) j) 2 (MeasureTheory.volume.restrict (ballSector x₀ r S sigma))) (hv : Ported.IsMatrixDivFormWeakSolutionZerothOrderOn a (ballSector x₀ r S sigma) v g 0) (T : Finset (Fin d)) : T ⊆ S → ∃ (w : HCPolySupport.H1Function (partialReflectedBallSector x₀ r S sigma T)) (b : HCPolySupport.CoeffField d) (h : HCPolySupport.Vec d → ℝ), Measurable b ∧ Ported.CoefficientIdentityDistanceLE (partialReflectedBallSector x₀ r S sigma T) b delta ∧ MeasureTheory.MemLp h 2 MeasureTheory.volume ∧ (∀ᵐ (y : HCPolySupport.Vec d), |h y| ≤ 2 ^ T.card * M) ∧ (∀ (j : Fin d), MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => HCPolySupport.matVecMul (b y) (w.grad y) j) 2 (MeasureTheory.volume.restrict (partialReflectedBallSector x₀ r S sigma T))) ∧ Ported.IsMatrixDivFormWeakSolutionZerothOrderOn b (partialReflectedBallSector x₀ r S sigma T) w h 0 ∧ (∀ y ∈ ballSector x₀ r S sigma, w.toFun y = v.toFun y) ∧ (∀ j ∈ T, ∀ (z : HCPolySupport.Vec d), w.toFun (HCPolySupport.coordFaceReflection (x₀ j) j z) = -w.toFun z) ∧ HCPolySupport.LocalizedZeroTraceFunctionOn (partialReflectedBallSector x₀ r S sigma T) (HCPolySupport.euclideanBall x₀ r) w.toFun

Odd unfolding of a sector weak solution. At every intermediate ball sector the odd extension solves the divergence-form equation for the conjugated coefficient with the oddly extended source, retains the small-contrast bound, restricts to the original datum, is odd under every unfolded face reflection, and keeps the localized zero-trace property needed by the next step.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.exists_oddReflection_weakSolution_ball {d : ℕ} {x₀ : HCPolySupport.Vec d} {r : ℝ} (hr : 0 < r) {S : Finset (Fin d)} {sigma : Fin d → ℝ} (hsigma : ∀ i ∈ S, |sigma i| = 1) {a : HCPolySupport.CoeffField d} {delta M : ℝ} (hM : 0 ≤ M) (hameas : Measurable a) (hcontrast : Ported.CoefficientIdentityDistanceLE (ballSector x₀ r S sigma) a delta) (v : HCPolySupport.H1Function (ballSector x₀ r S sigma)) (hzt : HCPolySupport.LocalizedZeroTraceFunctionOn (ballSector x₀ r S sigma) (HCPolySupport.euclideanBall x₀ r) v.toFun) {g : HCPolySupport.Vec d → ℝ} (hgL2 : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (ballSector x₀ r S sigma))) (hgM : ∀ᵐ (y : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (ballSector x₀ r S sigma), |g y| ≤ M) (hflux : ∀ (j : Fin d), MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => HCPolySupport.matVecMul (a y) (v.grad y) j) 2 (MeasureTheory.volume.restrict (ballSector x₀ r S sigma))) (hv : Ported.IsMatrixDivFormWeakSolutionZerothOrderOn a (ballSector x₀ r S sigma) v g 0) : ∃ (w : HCPolySupport.H1Function (HCPolySupport.euclideanBall x₀ r)) (b : HCPolySupport.CoeffField d) (h : HCPolySupport.Vec d → ℝ), Measurable b ∧ Ported.CoefficientIdentityDistanceLE (HCPolySupport.euclideanBall x₀ r) b delta ∧ Ported.MemScalarLInfOn (HCPolySupport.euclideanBall x₀ r) h ∧ Ported.IsMatrixDivFormWeakSolutionZerothOrderOn b (HCPolySupport.euclideanBall x₀ r) w h 0 ∧ (∀ y ∈ ballSector x₀ r S sigma, w.toFun y = v.toFun y) ∧ ∀ j ∈ S, ∀ (z : HCPolySupport.Vec d), w.toFun (HCPolySupport.coordFaceReflection (x₀ j) j z) = -w.toFun z

The odd reflection across all flat faces solves a small-contrast equation on the whole centred ball. This is the T = S case of the chain, transported along the identification of the fully unfolded sector with the ball.