CentralChildCaccioppoli

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

Coarse-grained Caccioppoli energy on the ordinary central child

The Chapter 3 public interior Caccioppoli endpoint of the homogenization development controls the centered patch at scale Q.scale - 2, namely caccioppoliCoreSet Q (cubeCenter Q) = \cu_m \cap (x_Q + \cu_{m-2}). The Section 3.5 argument of ABK26 instead uses the ordinary central child at scale Q.scale - 1. This module supplies that endpoint, for an arbitrary Chapter 2 cube solution and at every integer scale, and then specializes it to the canonical maximizer of a cube.

The deterministic content is already available upstream: the raw scale-zero Caccioppoli bridge estimates the localized one-third interior profile of the energy density, and the ordinary central child sits inside the concentric closed one-third subcube. Comparing normalizations costs exactly the parent to child volume ratio 3^d.

The right-hand side is the upstream interiorCaccioppoliRHS, i.e. the caccioppoliPrefactor — which already carries the explicit 3^{-2m} weight and the coarse-grained ThetaRatio/LambdaS factors — multiplied by the parent-cube oscillation L^2 square. No microscopic diffusivity enters.

Geometry of the ordinary central child

theorem Algsuperdiff.Section3.Provider.Besov.openCubeSet_centralChild_subset {d : ℕ} (Q : HCPolySupport.TriadicCube d) : HCPolySupport.openCubeSet (HCPolySupport.CubeCalderonZygmund.centralChild Q) ⊆ HCPolySupport.openCubeSet Q

The ordinary central child of Q sits inside Q.

theorem Algsuperdiff.Section3.Provider.Besov.openCubeSet_centralChild_subset_scaledClosedCubeSet_one_third {d : ℕ} (Q : HCPolySupport.TriadicCube d) : HCPolySupport.openCubeSet (HCPolySupport.CubeCalderonZygmund.centralChild Q) ⊆ HCPolySupport.scaledClosedCubeSet Q (1 / 3)

The ordinary central child is contained in the closed concentric one-third subcube, which is the localization radius occurring in the upstream raw centered Caccioppoli bridge.

theorem Algsuperdiff.Section3.Provider.Besov.centralChild_dilateCube {d : ℕ} (k : ℤ) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.CubeCalderonZygmund.centralChild (HCPolySupport.Book.Ch02.dilateCube k Q) = HCPolySupport.Book.Ch02.dilateCube k (HCPolySupport.CubeCalderonZygmund.centralChild Q)

Dilation commutes with taking the ordinary central child.

The central-child energy

noncomputable def Algsuperdiff.Section3.Provider.Besov.centralChildCaccioppoliEnergy {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (u : HCPolySupport.Book.Ch03.CubeSolution Q a) : ℝ

The parent-coefficient energy of a cube solution on the ordinary central child, normalized by the child volume. This is the quantity written \fint_{\cu_{m-1}} \nabla v \cdot \s \nabla v.

Equations

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

theorem Algsuperdiff.Section3.Provider.Besov.centralChildCaccioppoliEnergy_le_three_pow_mul_localizedProfile {d : ℕ} [NeZero d] {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} (u : HCPolySupport.Book.Ch03.CubeSolution Q a) : centralChildCaccioppoliEnergy Q a u ≤ 3 ^ d * HCPolySupport.coarseCaccioppoliLocalizedEnergyRadiusProfile Q (fun (y : HCPolySupport.Vec d) => HCPolySupport.scalarVariationEnergyIntegrand (HCPolySupport.Book.Ch03.pointwiseCoeffFor Q a) u.toPointwiseAHarmonic y) (1 / 3)

The ordinary central-child energy is bounded by 3^d times the raw localized one-third energy profile of the same solution. The factor is exactly the ratio of the parent and child volumes.

The central-child Caccioppoli endpoint

theorem Algsuperdiff.Section3.Provider.Besov.centralChildCaccioppoli_scale_zero (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 < C ∧ ∀ {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {s t : ℝ} (u : HCPolySupport.Book.Ch03.CubeSolution Q a), 0 < s → 0 < t → s + t < 1 → Q.scale = 0 → centralChildCaccioppoliEnergy Q a u ≤ HCPolySupport.Book.Ch03.interiorCaccioppoliRHS C Q a s t u

Scale-zero central-child Caccioppoli endpoint. The constant is dimension-only; it is the upstream scale-zero scalar envelope multiplied by d^2, and the only new geometric factor relative to the upstream centered core estimate is the parent-to-child volume ratio.

theorem Algsuperdiff.Section3.Provider.Besov.centralChildCaccioppoli_transport (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 < C ∧ ∀ {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {s t : ℝ} (u : HCPolySupport.Book.Ch03.CubeSolution Q a), 0 < s → 0 < t → s + t < 1 → centralChildCaccioppoliEnergy Q a u ≤ HCPolySupport.Book.Ch03.interiorCaccioppoliRHS C Q a s t u

Central-child coarse-grained Caccioppoli estimate at every integer scale. For a Chapter 2 cube solution on \cu_m, the coefficient energy on the ordinary central child \cu_{m-1} is bounded by the public Caccioppoli right-hand side of the parent, i.e. by the caccioppoliPrefactor — which carries the explicit 3^{-2m} weight — times the parent-cube oscillation L^2 square. The constant is dimension-only.

Dilation preserves the parent-coefficient central-child energy exactly and preserves the right-hand side after the 3^{-2m} factor is combined with the squared solution-amplitude normalization.

The canonical maximizer of a cube

noncomputable def Algsuperdiff.Section3.Provider.Besov.canonicalCubeMaximizerSolution {d : ℕ} (a : HCPolySupport.RegCoeffField d) (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (Q : HCPolySupport.TriadicCube d) (p q : HCPolySupport.Vec d) : HCPolySupport.Book.Ch03.CubeSolution Q (HCPolySupport.Book.Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha)

The canonical maximizer of the cube Q for the pair (p, q), read as a Chapter 2 cube solution of the coefficient family of a. This is the function written v = v(\cdot, \cu_m, p, q) in Section 3.5.

Equations

• Algsuperdiff.Section3.Provider.Besov.canonicalCubeMaximizerSolution a ha Q p q = (HCPolySupport.Book.Ch02.canonicalMaximizer ⋯ p q).toSolution

theorem Algsuperdiff.Section3.Provider.Besov.centralChildCaccioppoli_canonicalMaximizer (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 < C ∧ ∀ (a : HCPolySupport.RegCoeffField d) (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (Q : HCPolySupport.TriadicCube d) (p q : HCPolySupport.Vec d) {s t : ℝ}, 0 < s → 0 < t → s + t < 1 → centralChildCaccioppoliEnergy Q (HCPolySupport.Book.Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) (canonicalCubeMaximizerSolution a ha Q p q) ≤ HCPolySupport.Book.Ch03.interiorCaccioppoliRHS C Q (HCPolySupport.Book.Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) s t (canonicalCubeMaximizerSolution a ha Q p q)

The Section 3.5 form of the Caccioppoli step. For the canonical maximizer v of the cube \cu_m and an a.e. locally uniformly elliptic coefficient field, the coefficient energy of v on the ordinary central child \cu_{m-1} is bounded by the public Caccioppoli right-hand side of \cu_m, whose prefactor carries the explicit weight 3^{-2m} and whose remaining factor is the parent-cube oscillation L^2 square of v. The constant is dimension-only.