Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.InputSpecializations .FaithfulDescendant

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

theorem HCPolySupport.faithful_centered_descendant_product_le_parent_theta {d : ℕ} [NeZero d] {Q R : TriadicCube d} {j : ℕ} (a : CoeffField d) {s t lam Lam : ℝ} (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hR : R ∈ descendantsAtDepth Q j) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : Real.rpow 3 (-↑j) * ((LambdaSq R s (MultiscaleExponent.finite 1) a).rpow (1 / 2) * (lambdaSq R (1 - s) (MultiscaleExponent.finite 1) a).rpow (-1 / 2)) ≤ Real.rpow 3 (-coarseCaccioppoliSigma s t * ↑j) * (ThetaRatio Q s t a).rpow (1 / 2)

Descendant version of the coefficient localization displayed after the single-cube estimate in the notes, for the centered ellipticity product.

theorem HCPolySupport.faithful_centered_descendant_product_one_le_parent_theta {d : ℕ} [NeZero d] {Q R : TriadicCube d} {j : ℕ} (a : CoeffField d) {s t lam Lam : ℝ} (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hR : R ∈ descendantsAtDepth Q j) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : Real.rpow 3 (-↑j) * ((LambdaSq R s (MultiscaleExponent.finite 1) a).rpow (1 / 2) * (lambdaSq R 1 (MultiscaleExponent.finite 1) a).rpow (-1 / 2)) ≤ Real.rpow 3 (-coarseCaccioppoliSigma s t * ↑j) * (ThetaRatio Q s t a).rpow (1 / 2)

Variant of faithful_centered_descendant_product_le_parent_theta with lambdaSq R 1 in the inverse slot.

This is the structural line needed by the average part of the exact centered coefficient, whose local canonical A^\circ_1(R) contains lambdaSq R 1. Since 1 - s < 1, the inverse lambda monotonicity upgrades the 1 slot to the centered 1 - s slot before applying the usual descendant theta localization.

theorem HCPolySupport.faithful_centered_scale_mul_le_workGap_of_triadicGapScaleChoice {s C Cwork ρ₁ ρ₂ : ℝ} {k : ℕ} (hC : 0 ≤ C) (hwork : 81 * C ≤ Cwork) (hs : 0 < s) (hs1 : s < 1) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hlt : ρ₁ < ρ₂) : C / (s * (1 - s)) * Real.rpow 3 ↑k ≤ Cwork / (s * (1 - s)) * coarseCaccioppoliGapInv ρ₁ ρ₂

Centered-coefficient variant of faithful_scale_mul_le_workGap_of_triadicGapScaleChoice, with the harmless factor 1 / (s * (1 - s)) carried along.

theorem HCPolySupport.faithful_scale_mul_rpow_s_le_workGap_of_triadicGapScaleChoice {s C Cwork ρ₁ ρ₂ : ℝ} {k : ℕ} (hC : 0 ≤ C) (hwork : 81 * Real.rpow 3 s * C ≤ Cwork) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hlt : ρ₁ < ρ₂) : C * Real.rpow 3 ↑k * Real.rpow 3 s ≤ Cwork * coarseCaccioppoliGapInv ρ₁ ρ₂

Constant-branch scale absorption with the extra 3^s ceiling loss.

theorem HCPolySupport.faithful_integerized_height_depth_le_height_add_one {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s t C : ℝ} (hs : 0 < s) (k : ℕ) : ↑(coarseCaccioppoliBoundaryLocalizedExplicitHeightDepthAtScale Q a s t C k) ≤ coarseCaccioppoliBoundaryLocalizedExplicitHeightAtScale Q a s t C k + 1

A ceiling estimate for the integerized localized small-cube height.

theorem HCPolySupport.boundaryCrossCoeff_one_mul_le_boundaryCrossCoeff_of_cubeLpNorm_le_sqrt {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s C uL2Sq ρ₁ ρ₂ U : ℝ} {h : ℝ → ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (hlt : ρ₁ < ρ₂) (hU : U ≤ √uL2Sq) : coarseCaccioppoliBoundaryCrossCoeffOfHeight Q a s C 1 h ρ₁ ρ₂ * U ≤ coarseCaccioppoliBoundaryCrossCoeffOfHeight Q a s C uL2Sq h ρ₁ ρ₂

The unit-L² cross coefficient times a parent L² bound is controlled by the public cross coefficient. This is the finite-Cauchy bookkeeping used in the faithful small-cube proof: local descendant L² norms are summed first, then the parent L² size is inserted.

theorem HCPolySupport.faithful_constant_descendant_coeff_le_cross_of_scale_height_le_depth {d : ℕ} [NeZero d] {Q R : TriadicCube d} {j : ℕ} (a : CoeffField d) {s C Cwork k uL2Sq ρ₁ ρ₂ lam Lam : ℝ} {h : ℝ → ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (hs1 : s < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hR : R ∈ descendantsAtDepth Q j) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hscaleC : C * Real.rpow 3 k * Real.rpow 3 s ≤ Cwork * coarseCaccioppoliGapInv ρ₁ ρ₂) (hj_le : ↑j ≤ h ρ₁ ρ₂ + 1) : coarseCaccioppoliSingleCubeBoundaryConstantCoeff R a C k uL2Sq ≤ coarseCaccioppoliBoundaryCrossCoeffOfHeight Q a s Cwork uL2Sq h ρ₁ ρ₂

Descendant constant coefficient localization against the real localized height, with the ceiling loss isolated in hscaleC.

theorem HCPolySupport.faithful_constant_descendant_coeff_le_cross_of_scale_height_add_two_le_depth {d : ℕ} [NeZero d] {Q R : TriadicCube d} {j : ℕ} (a : CoeffField d) {s C Cwork k uL2Sq ρ₁ ρ₂ lam Lam : ℝ} {h : ℝ → ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (hs1 : s < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hR : R ∈ descendantsAtDepth Q j) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hscaleC : C * Real.rpow 3 k * Real.rpow 3 (2 * s) ≤ Cwork * coarseCaccioppoliGapInv ρ₁ ρ₂) (hj_le : ↑j ≤ h ρ₁ ρ₂ + 2) : coarseCaccioppoliSingleCubeBoundaryConstantCoeff R a C k uL2Sq ≤ coarseCaccioppoliBoundaryCrossCoeffOfHeight Q a s Cwork uL2Sq h ρ₁ ρ₂

Depth-plus-one version of faithful_constant_descendant_coeff_le_cross_of_scale_height_le_depth.

The arbitrary-center local-patch route takes descendants one generation deeper than the integerized height. The constant branch therefore needs one extra factor 3^s in the work-constant budget.

theorem HCPolySupport.faithful_centered_descendant_coeff_le_alpha_of_scale_height_le_depth {d : ℕ} [NeZero d] {Q R : TriadicCube d} {j : ℕ} (a : CoeffField d) {s t C Cwork k ρ₁ ρ₂ lam Lam : ℝ} {h : ℝ → ℝ → ℝ} (hC : 0 ≤ C) (hCwork : 0 ≤ Cwork) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hR : R ∈ descendantsAtDepth Q j) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hlt : ρ₁ < ρ₂) (hscaleC : C / (s * (1 - s)) * Real.rpow 3 k ≤ Cwork / (s * (1 - s)) * coarseCaccioppoliGapInv ρ₁ ρ₂) (hh_le : h ρ₁ ρ₂ ≤ ↑j) : coarseCaccioppoliSingleCubeBoundaryCenteredCoeff R a s C k ↑j ≤ coarseCaccioppoliBoundaryAlphaOfHeight Q a s t Cwork h ρ₁ ρ₂

The centered faithful coefficient produced at the integerized depth is bounded by the parent alpha coefficient at the real localized height.