Coarse-graining support:

Support.Sobolev.Foundations.CubeCalderonZygmund.HarmonicGradientGainIteration

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Internal exponent-raising carrier for harmonic gradients

The declarations in INTERNAL are an induction carrier, not a source-facing Calderón--Zygmund assumption. Its membership field is kept alongside the normalized extended-norm estimate because the next Sobolev step must construct a genuine W^{1,p} witness; finiteness must never be silently reintroduced as a caller hypothesis.

structure HCPolySupport.CubeCalderonZygmund.INTERNAL.HarmonicGradientGain (d : ℕ) (r : FiniteLpExponent) (depth : ℕ) : Type

The proved induction carrier for a harmonic-gradient integrability gain. It is deliberately an explicit structure rather than an opaque predicate: its only analytic data are the stated membership and bound, both quantified over all harmonic cube solutions.

• constantValue : ENNReal

  The positive finite factor bounding each gradient coordinate in normalized L^r by the sum of the parent cube coordinate L² norms.

• constant_pos : 0 < self.constantValue
• constant_ne_top : self.constantValue ≠ ⊤
• memLp (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) : (WeakPoissonEquationOn (openCubeSet Q) u fun (x : Vec d) => 0) → ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => u.grad x i) r.exponent (normalizedCubeMeasure (centralDescendant Q depth))
• bound (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) : (WeakPoissonEquationOn (openCubeSet Q) u fun (x : Vec d) => 0) → ∀ (i : Fin d), MeasureTheory.eLpNorm (fun (x : Vec d) => u.grad x i) r.exponent (normalizedCubeMeasure (centralDescendant Q depth)) ≤ self.constantValue * ∑ j : Fin d, MeasureTheory.eLpNorm (fun (x : Vec d) => u.grad x j) 2 (normalizedCubeMeasure Q)

structure HCPolySupport.CubeCalderonZygmund.INTERNAL.HarmonicEuclideanGradientGain (d : ℕ) (r : FiniteLpExponent) (depth : ℕ) : Type

Euclidean-facing form of the internal carrier. This is the API consumed by vector-valued good-λ arguments; no caller supplies coordinate measurability data.

• constantValue : ENNReal

  The finite factor bounding the Euclidean gradient in normalized L^r by the sum of the parent cube coordinate L² norms.

• constant_ne_top : self.constantValue ≠ ⊤
• memLp (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) : (WeakPoissonEquationOn (openCubeSet Q) u fun (x : Vec d) => 0) → MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (u.grad x)) r.exponent (normalizedCubeMeasure (centralDescendant Q depth))
• bound (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) : (WeakPoissonEquationOn (openCubeSet Q) u fun (x : Vec d) => 0) → MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (u.grad x)) r.exponent (normalizedCubeMeasure (centralDescendant Q depth)) ≤ self.constantValue * ∑ j : Fin d, MeasureTheory.eLpNorm (fun (x : Vec d) => u.grad x j) 2 (normalizedCubeMeasure Q)

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.harmonicGradientGainL2DepthZero (d : ℕ) : HarmonicGradientGain d FiniteLpExponent.two 0

The unraised base of the induction carrier: normalized L² control at depth zero costs exactly one.

Equations

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

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.HarmonicEuclideanGradientGain.fromScalar {d : ℕ} {r : FiniteLpExponent} {depth : ℕ} (G : HarmonicGradientGain d r depth) : HarmonicEuclideanGradientGain d r depth

Convert coordinate gradient gains into a Euclidean gain at the same exponent and depth, multiplying the scalar bound constant by two dimension factors.

Equations

• HCPolySupport.CubeCalderonZygmund.INTERNAL.HarmonicEuclideanGradientGain.fromScalar G = { constantValue := ‖↑d‖ₑ * ↑d * G.constantValue, constant_ne_top := ⋯, memLp := ⋯, bound := ⋯ }

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.memLpOn_openCubeSet_of_memLp_normalizedCubeMeasure {d : ℕ} (Q : TriadicCube d) {p : ENNReal} {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f p (normalizedCubeMeasure Q)) : MeasureTheory.MemLp f p (volumeMeasureOn (openCubeSet Q))

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.normalized_cubeSobolevEmbedding_finiteLp {d : ℕ} (hd : 0 < d) (r q : FiniteLpExponent) (hqr : q.exponent.toReal⁻¹ = r.exponent.toReal⁻¹ - (↑d)⁻¹) (hrlt : r.exponent.toReal < ↑d) : ∃ (C : ENNReal), 0 < C ∧ C ≠ ⊤ ∧ ∀ (Q : TriadicCube d) (v : W1pFunction (openCubeSet Q) r.exponent), MeasureTheory.eLpNorm v.toFun q.exponent (normalizedCubeMeasure Q) ≤ C * (ENNReal.ofReal (cubeScaleFactor Q) * ∑ j : Fin d, MeasureTheory.eLpNorm (fun (x : Vec d) => v.grad x j) r.exponent (normalizedCubeMeasure Q) + MeasureTheory.eLpNorm v.toFun r.exponent (normalizedCubeMeasure Q))

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.ennreal_le_of_toReal_le {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) (h : a.toReal ≤ b.toReal) : a ≤ b

Lift an inequality between real realizations of finite extended norms back to ℝ≥0∞. All finiteness is explicit, so the induction carrier never turns an extended-norm comparison into an implicit integrability hypothesis.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.centralChild_normalized_hessian_energy_bound_ennreal {d : ℕ} : ∃ (A : ENNReal), 0 < A ∧ A ≠ ⊤ ∧ ∀ (Q : TriadicCube d) (u : H1Function (openCubeSet Q)), (WeakPoissonEquationOn (openCubeSet Q) u fun (x : Vec d) => 0) → ∃ (uS : H1Function (scaledOpenCubeSet Q (1 / 2))), uS.toFun = u.toFun ∧ uS.grad = u.grad ∧ ∃ (H : HasWeakHessianOn (scaledOpenCubeSet Q (1 / 2)) uS), ENNReal.ofReal (cubeScaleFactor (centralChild Q)) * ∑ i : Fin d, ∑ j : Fin d, MeasureTheory.eLpNorm (fun (x : Vec d) => H.hess i j x) 2 (normalizedCubeMeasure (centralChild Q)) ≤ A * ∑ j : Fin d, MeasureTheory.eLpNorm (fun (x : Vec d) => u.grad x j) 2 (normalizedCubeMeasure Q)

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.centralDescendant_scaleFactor_le {d : ℕ} (Q : TriadicCube d) (n : ℕ) : ENNReal.ofReal (cubeScaleFactor (centralDescendant Q n)) ≤ ENNReal.ofReal (cubeScaleFactor Q)

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.sum_fin_le_natCast_mul {d : ℕ} (f : Fin d → ENNReal) (A : ENNReal) (h : ∀ (i : Fin d), f i ≤ A) : ∑ i : Fin d, f i ≤ ↑d * A

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.row_sum_le_double_sum {d : ℕ} (f : Fin d → Fin d → ENNReal) (i : Fin d) : ∑ j : Fin d, f i j ≤ ∑ k : Fin d, ∑ j : Fin d, f k j

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.hessianGradCoordToW1p {d : ℕ} {U : Set (Vec d)} {u : H1Function U} (H : HasWeakHessianOn U u) (i : Fin d) (p : FiniteLpExponent) (hvalue : MeasureTheory.MemLp (fun (x : Vec d) => u.grad x i) p.exponent (MeasureTheory.volume.restrict U)) (hgrad : ∀ (j : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => H.hess i j x) p.exponent (MeasureTheory.volume.restrict U)) : W1pFunction U p.exponent

Package gradient coordinate i as a W^{1,p} function with weak gradient given by Hessian row i, using the supplied L^p membership proofs.

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.centralDescendant_after_centralChild {d : ℕ} (Q : TriadicCube d) (n : ℕ) : centralDescendant (centralChild Q) n = centralDescendant Q (n + 1)

The exact depth identity used in the derivative branch of the gain upgrade.

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.scaled_row_sum_le_dimension_mul_energy {d : ℕ} (values : Fin d → ENNReal) (energy : Fin d → Fin d → ENNReal) (i : Fin d) {childScale parentScale coefficient A R : ENNReal} (hvalues : ∀ (j : Fin d), values j ≤ coefficient * ∑ k : Fin d, energy i k) (hscale : childScale ≤ parentScale) (henergy : parentScale * ∑ a : Fin d, ∑ b : Fin d, energy a b ≤ A * R) : childScale * ∑ j : Fin d, values j ≤ ↑d * coefficient * A * R

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.HarmonicGradientGain.upgrade {d : ℕ} (hd : 0 < d) {r q : FiniteLpExponent} (hqr : q.exponent.toReal⁻¹ = r.exponent.toReal⁻¹ - (↑d)⁻¹) (hrlt : r.exponent.toReal < ↑d) {depth : ℕ} (G : HarmonicGradientGain d r depth) : HarmonicGradientGain d q (depth + 1)

One source-faithful Sobolev step in the internal harmonic-gradient iteration. The derivative harmonicity and Hessian witness are both produced inside the proof; callers supply only the preceding gain carrier.

Equations

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

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.HarmonicGradientGain.downgrade {d : ℕ} {r s : FiniteLpExponent} {depth : ℕ} (G : HarmonicGradientGain d r depth) (hsr : s.exponent ≤ r.exponent) : HarmonicGradientGain d s depth

Lowering the exponent on a probability-normalized cube preserves an internal gain carrier without changing its analytic constant.

Equations

• G.downgrade hsr = { constantValue := G.constantValue, constant_pos := ⋯, constant_ne_top := ⋯, memLp := ⋯, bound := ⋯ }

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.sobolevLadderExponent (d : ℕ) (hd : 2 ≤ d) (n : ℕ) (hn : 2 * n < d) : FiniteLpExponent

The explicit finite Sobolev ladder used above the L² base. The side condition is precisely the positivity of its denominator.

Equations

• HCPolySupport.CubeCalderonZygmund.INTERNAL.sobolevLadderExponent d hd n hn = { exponent := ENNReal.ofReal (2 * ↑d / (↑d - 2 * ↑n)), one_lt := ⋯, lt_top := ⋯ }

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.sobolevLadderExponent_step_relation (d : ℕ) (hd : 2 ≤ d) (n : ℕ) (hn : 2 * (n + 1) < d) : (sobolevLadderExponent d hd (n + 1) hn).exponent.toReal⁻¹ = (sobolevLadderExponent d hd n ⋯).exponent.toReal⁻¹ - (↑d)⁻¹

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.sobolevLadderExponent_lt_dimension (d : ℕ) (hd : 2 ≤ d) (n : ℕ) (hn : 2 * (n + 1) < d) : (sobolevLadderExponent d hd n ⋯).exponent.toReal < ↑d

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.sobolevLadderExponent_zero (d : ℕ) (hd : 2 ≤ d) : sobolevLadderExponent d hd 0 ⋯ = FiniteLpExponent.two

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.harmonicGradientGainLadder (d : ℕ) (hd : 3 ≤ d) (n : ℕ) (hn : 2 * n < d) : HarmonicGradientGain d (sobolevLadderExponent d ⋯ n hn) n

Iterate the harmonic gradient Sobolev gain from L² to exponent 2 * d / (d - 2 * n) at depth n, for d ≥ 3 and 2 * n < d.

Equations

• One or more equations did not get rendered due to their size.
• HCPolySupport.CubeCalderonZygmund.INTERNAL.harmonicGradientGainLadder d hd 0 hn = ⋯.mpr (HCPolySupport.CubeCalderonZygmund.INTERNAL.harmonicGradientGainL2DepthZero d)

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.terminalLadderDepth_twice_lt (d : ℕ) (hd : 3 ≤ d) : 2 * ((d - 1) / 2) < d

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.targetSobolevSourceExponent (d : ℕ) (hd2 : 2 ≤ d) (q : FiniteLpExponent) (hq : 2 < q.exponent.toReal) : FiniteLpExponent

The finite source exponent d * q / (d + q) whose Sobolev conjugate is the target q, for dimension at least two and target exponent greater than two.

Equations

• HCPolySupport.CubeCalderonZygmund.INTERNAL.targetSobolevSourceExponent d hd2 q hq = { exponent := ENNReal.ofReal (↑d * q.exponent.toReal / (↑d + q.exponent.toReal)), one_lt := ⋯, lt_top := ⋯ }

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.targetSobolevSourceExponent_lt_dimension (d : ℕ) (hd2 : 2 ≤ d) (q : FiniteLpExponent) (hq : 2 < q.exponent.toReal) : (targetSobolevSourceExponent d hd2 q hq).exponent.toReal < ↑d

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.targetSobolevSourceExponent_relation (d : ℕ) (hd2 : 2 ≤ d) (q : FiniteLpExponent) (hq : 2 < q.exponent.toReal) : q.exponent.toReal⁻¹ = (targetSobolevSourceExponent d hd2 q hq).exponent.toReal⁻¹ - (↑d)⁻¹

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.targetSobolevSourceExponent_le_two_twoDim (q : FiniteLpExponent) (hq : 2 < q.exponent.toReal) : (targetSobolevSourceExponent 2 targetSobolevSourceExponent_le_two_twoDim._proof_1 q hq).exponent ≤ 2

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.harmonicGradientGainAboveTwoInDimensionTwo (q : FiniteLpExponent) (hq2 : 2 < q.exponent) : HarmonicGradientGain 2 q 1

In dimension two, one final finite Sobolev step from the downgraded L² base reaches every target above two.

Equations

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

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.harmonicEuclideanGradientGainAboveTwoInDimensionTwo (q : FiniteLpExponent) (hq2 : 2 < q.exponent) : HarmonicEuclideanGradientGain 2 q 1

Construct the Euclidean harmonic gradient gain at depth one in dimension two for any finite target exponent greater than two.

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.targetSobolevSourceExponent_le_terminalLadder (d : ℕ) (hd : 3 ≤ d) (q : FiniteLpExponent) (hq : 2 < q.exponent.toReal) : (targetSobolevSourceExponent d ⋯ q hq).exponent ≤ (sobolevLadderExponent d ⋯ ((d - 1) / 2) ⋯).exponent

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.harmonicGradientGainAboveTwoInDimensionAtLeastThree (d : ℕ) (hd : 3 ≤ d) (q : FiniteLpExponent) (hq2 : 2 < q.exponent) : HarmonicGradientGain d q ((d - 1) / 2 + 1)

The final Sobolev step from the terminal ladder exponent.

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.nonempty_harmonicGradientGain_finiteTarget_of_three_le (d : ℕ) (hd : 3 ≤ d) (q : FiniteLpExponent) : Nonempty ((depth : ℕ) × HarmonicGradientGain d q depth)

Every finite target exponent is reached in dimension at least three.

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.harmonicEuclideanGradientGainAboveTwoInDimensionAtLeastThree (d : ℕ) (hd : 3 ≤ d) (q : FiniteLpExponent) (hq2 : 2 < q.exponent) : HarmonicEuclideanGradientGain d q ((d - 1) / 2 + 1)

Vector-facing arbitrary finite target gain in dimensions at least three. Its membership and bound are in the HilbertVec.ofVec representation used by the stopping-time layer; all coordinate measurability is discharged inside fromScalar.

Equations

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

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.harmonicEuclideanGradientGainAtMostTwo (d : ℕ) (q : FiniteLpExponent) (hq2 : q.exponent ≤ 2) : HarmonicEuclideanGradientGain d q 0

Vector-facing normalized L^q gain for every target at or below L².

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.nonempty_harmonicEuclideanGradientGain_finiteTarget_of_two_le (d : ℕ) (hd : 2 ≤ d) (q : FiniteLpExponent) : Nonempty ((depth : ℕ) × HarmonicEuclideanGradientGain d q depth)

Dimension-at-least-two public availability statement for the Euclidean gain API. It is deliberately Nonempty Σ because the depth is analytic data of the construction, not a hypothesis that callers must provide.

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.harmonicGradientGainInDimensionOne (p : FiniteLpExponent) : HarmonicGradientGain 1 p 1

One-dimensional finite-target carrier, obtained from the source theorem's real bound only after the accompanying source-level MemLp witness has made both ENNReal sides finite.

Equations

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

noncomputable def HCPolySupport.CubeCalderonZygmund.INTERNAL.harmonicEuclideanGradientGainInDimensionOne (p : FiniteLpExponent) : HarmonicEuclideanGradientGain 1 p 1

Construct the Euclidean harmonic gradient gain at depth one in dimension one for any finite target exponent.

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.nonempty_harmonicEuclideanGradientGain_finiteTarget_of_pos (d : ℕ) (hd : 0 < d) (q : FiniteLpExponent) : Nonempty ((depth : ℕ) × HarmonicEuclideanGradientGain d q depth)

All positive dimensions now expose the Euclidean finite-target carrier. The depth is returned as construction data, not a caller hypothesis.