Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.Basic

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

Deterministic coarse-grained Caccioppoli backbones

This file isolates the radius-iteration backbone of the Chapter-3 coarse Caccioppoli estimate.

At the current checkpoint the cutoff/Besov argument producing the local recursive inequality is still upstream work. The theorems here therefore keep that step as an explicit hypothesis and package the quantitative iteration and multiscale prefactors that consume it.

theorem HCPolySupport.mul_one_sub_nonneg {s : ℝ} (h0 : 0 ≤ s) (h1 : s ≤ 1) : 0 ≤ s * (1 - s)

Small real-arithmetic helper: s * (1 - s) ≥ 0 whenever 0 ≤ s ≤ 1. Used in several coarse-Caccioppoli non-negativity chains.

def HCPolySupport.coarseCaccioppoliSigma (s t : ℝ) : ℝ

The Chapter-3 gap parameter σ = 1 - s - t.

Equations

• HCPolySupport.coarseCaccioppoliSigma s t = 1 - s - t

noncomputable def HCPolySupport.coarseCaccioppoliBeta (s t : ℝ) : ℝ

The recursion exponent β = 2 (1 - t) / (1 - s - t) appearing in the radius-iteration step of the coarse Caccioppoli proof.

Equations

• HCPolySupport.coarseCaccioppoliBeta s t = 2 * (1 - t) / HCPolySupport.coarseCaccioppoliSigma s t

noncomputable def HCPolySupport.coarseCaccioppoliPower (s t : ℝ) : ℝ

The note exponent 2s / (1 - s - t) attached to the recursive error prefactor.

Equations

• HCPolySupport.coarseCaccioppoliPower s t = 2 * s / HCPolySupport.coarseCaccioppoliSigma s t

def HCPolySupport.CoarseCaccioppoliRadiusBoundedAbove (F : ℝ → ℝ) : Prop

Upper boundedness on the radius interval used in the Chapter-3 radius-iteration argument.

Equations

• HCPolySupport.CoarseCaccioppoliRadiusBoundedAbove F = ∃ (B : ℝ), ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → F ρ ≤ B

def HCPolySupport.CoarseCaccioppoliRadiusRecurrence (F : ℝ → ℝ) (A β : ℝ) : Prop

The one-step recursive inequality produced by the local cutoff/Besov part of the coarse Caccioppoli proof.

Equations

• HCPolySupport.CoarseCaccioppoliRadiusRecurrence F A β = ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → F ρ₁ ≤ 1 / 2 * F ρ₂ + A * (ρ₂ - ρ₁).rpow (-β)

noncomputable def HCPolySupport.coarseCaccioppoliRadiusSequence (n : ℕ) : ℝ

The deterministic radius sequence ρ_n = 1 - 2 / (3 (n + 1)), starting at 1/3 and increasing to 1.

Equations

• HCPolySupport.coarseCaccioppoliRadiusSequence n = 1 - 2 / (3 * (↑n + 1))

def HCPolySupport.CoarseCaccioppoliRadiusSequenceRecurrence (F : ℝ → ℝ) (A β : ℝ) : Prop

The same recursive inequality specialized to the deterministic Chapter-3 radius sequence ρ_n. This is the concrete iteration interface needed when a local cutoff construction only supplies the consecutive pairs (ρ_n, ρ_{n+1}).

Equations

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

noncomputable def HCPolySupport.coarseCaccioppoliRadiusIterationTerm (β : ℝ) (n : ℕ) : ℝ

The nth weighted error term in the deterministic radius-iteration argument.

Equations

• HCPolySupport.coarseCaccioppoliRadiusIterationTerm β n = (1 / 2) ^ n * (HCPolySupport.coarseCaccioppoliRadiusSequence (n + 1) - HCPolySupport.coarseCaccioppoliRadiusSequence n).rpow (-β)

noncomputable def HCPolySupport.coarseCaccioppoliRadiusIterationConst (β : ℝ) : ℝ

The deterministic radius-iteration constant obtained by summing the geometric error terms coming from coarseCaccioppoliRadiusIterationTerm.

Equations

• HCPolySupport.coarseCaccioppoliRadiusIterationConst β = ∑' (n : ℕ), HCPolySupport.coarseCaccioppoliRadiusIterationTerm β n

noncomputable def HCPolySupport.coarseCaccioppoliBufferedCutoffRadius (ρ₁ ρ₂ : ℝ) : ℝ

Midpoint radius used by the buffered cutoff version of the coarse Caccioppoli single-step estimate.

Equations

• HCPolySupport.coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂ = (ρ₁ + ρ₂) / 2

theorem HCPolySupport.coarseCaccioppoliBufferedCutoffRadius_between {ρ₁ ρ₂ : ℝ} (hlt : ρ₁ < ρ₂) : ρ₁ < coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂ ∧ coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂ < ρ₂

theorem HCPolySupport.coarseCaccioppoliBufferedCutoffRadius_outer_gap (ρ₁ ρ₂ : ℝ) : ρ₂ - coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂ = (ρ₂ - ρ₁) / 2

theorem HCPolySupport.coarseCaccioppoliBufferedCutoffRadius_inner_gap (ρ₁ ρ₂ : ℝ) : coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂ - ρ₁ = (ρ₂ - ρ₁) / 2

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryRecursionRhs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) : ℝ

The note-facing recursive right-hand side in the boundary coarse Caccioppoli proof, after the local cutoff/Besov step has produced the radius-recursion with exponent coarseCaccioppoliBeta s t.

Equations

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

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryRecursionRhsSplit {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) : ℝ

Split version of the note-facing recursive right-hand side. Calpha controls the height/absorption branch, while Ccross controls the local cross coefficient. Keeping these separate prevents a centered-gradient budget from drifting into the purely local quadratic branch.

Equations

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

theorem HCPolySupport.coarseCaccioppoliBoundaryRecursionRhsSplit_self {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) : coarseCaccioppoliBoundaryRecursionRhsSplit Q a s t C C uL2Sq = coarseCaccioppoliBoundaryRecursionRhs Q a s t C uL2Sq

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) : ℝ

The first note-facing boundary coarse Caccioppoli prefactor obtained from the radius-iteration lemma under an explicit recursive hypothesis.

Equations

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

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryNoteRhs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) : ℝ

Literal normalized m = 0 right-hand side from the note's boundary coarse Caccioppoli proposition.

Here C represents the dimension-dependent constant in the note statement, not the intermediate projected-Poincare constant used by some lower-level single-cube wrappers.

Equations

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

noncomputable def HCPolySupport.coarseCaccioppoliInteriorBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) : ℝ

The current interior wrapper reuses the same radius-iteration constant and recursive prefactor as the boundary version once an interior recursive estimate has been supplied.

Equations

• HCPolySupport.coarseCaccioppoliInteriorBound Q a s t C uL2Sq = HCPolySupport.coarseCaccioppoliBoundaryBound Q a s t C uL2Sq

noncomputable def HCPolySupport.coarseCaccioppoliInteriorNoteRhs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) : ℝ

Literal normalized m = 0 right-hand side from the note's interior coarse Caccioppoli corollary.

Equations

• HCPolySupport.coarseCaccioppoliInteriorNoteRhs Q a s t C uL2Sq = HCPolySupport.coarseCaccioppoliBoundaryNoteRhs Q a s t C uL2Sq

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightRecursionRhs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) : ℝ

The honest pre-Besov recursive right-hand side obtained from the note's explicit height choice h = max {k + 4, ceil(...)}. The first summand records the k + 4 branch; the second records the logarithmic branch.

Equations

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

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightRecursionRhsSplit {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) : ℝ

Split explicit-height recursive right-hand side. The left branch only uses the cross/local constant Ccross; the logarithmic-height branch uses Calpha through the height choice and Ccross through the cross coefficient.

Equations

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

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightRecursionRhsSplit_self {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) : coarseCaccioppoliBoundaryExplicitHeightRecursionRhsSplit Q a s t C C uL2Sq = coarseCaccioppoliBoundaryExplicitHeightRecursionRhs Q a s t C uL2Sq

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) : ℝ

The boundary radius-iteration bound driven by the explicit-height recursive right-hand side above. This is the final pre-Besov boundary surface with no remaining extra cross-scale hypothesis.

Equations

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

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightBoundSplit {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) : ℝ

Split boundary radius-iteration bound driven by coarseCaccioppoliBoundaryExplicitHeightRecursionRhsSplit.

Equations

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

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightBoundSplit_self {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) : coarseCaccioppoliBoundaryExplicitHeightBoundSplit Q a s t C C uL2Sq = coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq

noncomputable def HCPolySupport.coarseCaccioppoliInteriorExplicitHeightBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) : ℝ

The interior pre-Besov explicit-height bound reuses the same recursive prefactor as the boundary version, once the centered local estimate has been transported into the iteration backbone.

Equations

• HCPolySupport.coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq = HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq

theorem HCPolySupport.coarseCaccioppoliInteriorExplicitHeightBound_le_noteRhs_of_boundary {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Cinternal Cnote uL2Sq : ℝ) (h : coarseCaccioppoliBoundaryExplicitHeightBound Q a s t Cinternal uL2Sq ≤ coarseCaccioppoliBoundaryNoteRhs Q a s t Cnote uL2Sq) : coarseCaccioppoliInteriorExplicitHeightBound Q a s t Cinternal uL2Sq ≤ coarseCaccioppoliInteriorNoteRhs Q a s t Cnote uL2Sq

def HCPolySupport.CoarseCaccioppoliRadiusAgreement (F G : ℝ → ℝ) : Prop

Agreement of two radius-dependent quantities on the interval used by the deterministic iteration. In the interior proof this packages the fact that centering v := u - (u)_Q does not change the gradient quantity being iterated.

Equations

• HCPolySupport.CoarseCaccioppoliRadiusAgreement F G = ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → F ρ = G ρ

def HCPolySupport.CoarseCaccioppoliBoundaryPreRecurrence {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (F : ℝ → ℝ) : Prop

Pre-absorption local input for the boundary coarse Caccioppoli proof: after the cutoff/Besov step and coefficient bookkeeping, the local estimate has an absorbable sqrt (F ρ₂) cross term whose square is controlled by the final note-facing recursion right-hand side.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundaryExplicitHeightPreRecurrence {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (F : ℝ → ℝ) : Prop

Pre-recurrence surface with the enlarged explicit-height recursion prefactor. This is the natural middle layer for localized height choices, whose cross term is controlled by coarseCaccioppoliBoundaryExplicitHeightRecursionRhs rather than by the smaller raw note prefactor.

Equations

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

def HCPolySupport.CoarseCaccioppoliInteriorPreRecurrence {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (F : ℝ → ℝ) : Prop

The current interior middle layer reuses the same pre-recurrence surface as the boundary version; the eventual difference is only in how the local estimate is produced.

Equations

• HCPolySupport.CoarseCaccioppoliInteriorPreRecurrence Q a s t C uL2Sq F = HCPolySupport.CoarseCaccioppoliBoundaryPreRecurrence Q a s t C uL2Sq F

def HCPolySupport.CoarseCaccioppoliInteriorExplicitHeightPreRecurrence {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (F : ℝ → ℝ) : Prop

Interior version of the explicit-height pre-recurrence surface.

Equations

• HCPolySupport.CoarseCaccioppoliInteriorExplicitHeightPreRecurrence Q a s t C uL2Sq F = HCPolySupport.CoarseCaccioppoliBoundaryExplicitHeightPreRecurrence Q a s t C uL2Sq F

def HCPolySupport.CoarseCaccioppoliBoundaryRawEstimate (F : ℝ → ℝ) (α B : ℝ → ℝ → ℝ) : Prop

Abstract local single-cube estimate before coefficient bookkeeping and Young absorption. The note's estimate e.cg.Caccioppoli.single.cube.boundary.deterministic.theory has exactly this shape.

Equations

• HCPolySupport.CoarseCaccioppoliBoundaryRawEstimate F α B = ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → F ρ₁ ≤ α ρ₁ ρ₂ * F ρ₂ + B ρ₁ ρ₂ * √(F ρ₂)

def HCPolySupport.CoarseCaccioppoliBoundaryCoefficientControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (α B : ℝ → ℝ → ℝ) : Prop

Abstract coefficient bookkeeping for the local single-cube estimate. This packages the note's choice of h and the conversion of localized coefficient factors into the final note-facing recursion right-hand side.

Equations

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

def HCPolySupport.CoarseCaccioppoliInteriorRawEstimate (F : ℝ → ℝ) (α B : ℝ → ℝ → ℝ) : Prop

The current interior middle layer uses the same abstract local single-cube surface as the boundary version.

Equations

• HCPolySupport.CoarseCaccioppoliInteriorRawEstimate F α B = HCPolySupport.CoarseCaccioppoliBoundaryRawEstimate F α B

def HCPolySupport.CoarseCaccioppoliInteriorCoefficientControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (α B : ℝ → ℝ → ℝ) : Prop

The current interior coefficient bookkeeping surface also matches the boundary one.

Equations

• HCPolySupport.CoarseCaccioppoliInteriorCoefficientControl Q a s t C uL2Sq α B = HCPolySupport.CoarseCaccioppoliBoundaryCoefficientControl Q a s t C uL2Sq α B

noncomputable def HCPolySupport.coarseCaccioppoliGapInv (ρ₁ ρ₂ : ℝ) : ℝ

The inverse gap factor appearing in the radius-recursion estimates.

Equations

• HCPolySupport.coarseCaccioppoliGapInv ρ₁ ρ₂ = (ρ₂ - ρ₁).rpow (-1)

def HCPolySupport.CoarseCaccioppoliTriadicGapScaleChoice (k : ℕ) (ρ₁ ρ₂ : ℝ) : Prop

The note's triadic scale choice for the gap ρ₂ - ρ₁: a natural scale k satisfying 3⁻⁴ (ρ₂ - ρ₁) ≤ 3⁻ᵏ ≤ 3⁻³ (ρ₂ - ρ₁).

Equations

• HCPolySupport.CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂ = (1 / 81 * (ρ₂ - ρ₁) ≤ (3 ^ k)⁻¹ ∧ (3 ^ k)⁻¹ ≤ 1 / 27 * (ρ₂ - ρ₁))

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryAlphaOfHeight {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (h : ℝ → ℝ → ℝ) (ρ₁ ρ₂ : ℝ) : ℝ

Note-shaped boundary coefficient in front of F ρ₂ after replacing the dyadic-scale factor by an inverse gap and keeping the auxiliary height choice h.

Equations

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

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryCrossCoeffOfHeight {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) (ρ₁ ρ₂ : ℝ) : ℝ

Note-shaped boundary cross coefficient in front of sqrt (F ρ₂) after replacing the dyadic-scale factor by an inverse gap and keeping the auxiliary height choice h.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundaryNoteRawEstimate {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) (F : ℝ → ℝ) : Prop

The current note-shaped raw boundary estimate: the local single-cube input has the note's coefficient structure, parameterized by the auxiliary height choice h.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundaryNoteRawEstimateSplit {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) (F : ℝ → ℝ) : Prop

Split version of the note-shaped raw boundary estimate. The absorption coefficient uses Calpha, while the cross coefficient uses the independent local budget Ccross.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundaryNoteCoefficientControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) : Prop

The current note-shaped boundary coefficient-control surface: the remaining task is to verify the note's explicit height choice implies this property.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundaryNoteAbsorptionCondition {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (h : ℝ → ℝ → ℝ) : Prop

The note-specific absorption obligation: the chosen auxiliary height makes the coefficient in front of F ρ₂ absorbable by the Young step.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundaryNoteCrossTermBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) : Prop

The note-specific cross-term bookkeeping obligation: after choosing the auxiliary height, the square of the remaining cross coefficient is controlled by the final recursion right-hand side.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundaryHeightChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (h : ℝ → ℝ → ℝ) : Prop

Note-facing explicit height bookkeeping for the boundary proof: for each gap ρ₂ - ρ₁, choose the triadic scale k from the note together with an auxiliary height h that is at least k + 4 and already makes the absorbable coefficient small. This isolates the first half of the note's h = max {…} construction without yet forcing the later 3^{s h} estimate.

Equations

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

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryHeightLogArg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℕ) : ℝ

The logarithmic argument in the note's explicit h = max {k+4, ceil(...)} choice.

Equations

• HCPolySupport.coarseCaccioppoliBoundaryHeightLogArg Q a s t C k = 4 * (C / (s * (1 - s)) * 3 ^ k * (HCPolySupport.ThetaRatio Q s t a).rpow (1 / 2))

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightAtScale {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℕ) : ℝ

The explicit height chosen in the note at a fixed triadic scale k. This packages the max {k + 4, ceil(...)} formula using a natural ceiling.

Equations

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

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℝ → ℝ → ℕ) : ℝ → ℝ → ℝ

The note's explicit h-choice obtained after selecting a triadic scale k = k(ρ₁, ρ₂) for each radius gap.

Equations

• HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k ρ₁ ρ₂ = HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightAtScale Q a s t C (k ρ₁ ρ₂)

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightAtScale {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℕ) : ℝ

A localized variant of the explicit height which keeps the note's height choice but also enforces the scale-localization lower bound h >= 4 / s. For t > 0, this also implies h >= 4 / (s + t).

Equations

• HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightAtScale Q a s t C k = max (HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightAtScale Q a s t C k) (4 / s)

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k : ℝ → ℝ → ℕ) : ℝ → ℝ → ℝ

Radius-indexed localized explicit height obtained from a scale choice.

Equations

• HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k ρ₁ ρ₂ = HCPolySupport.coarseCaccioppoliBoundaryLocalizedExplicitHeightAtScale Q a s t C (k ρ₁ ρ₂)

def HCPolySupport.CoarseCaccioppoliInteriorNoteRawEstimate {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) (F : ℝ → ℝ) : Prop

The interior note-shaped raw estimate currently reuses the same coefficient structure as the boundary version.

Equations

• HCPolySupport.CoarseCaccioppoliInteriorNoteRawEstimate Q a s t C uL2Sq h F = HCPolySupport.CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq h F

def HCPolySupport.CoarseCaccioppoliInteriorNoteRawEstimateSplit {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) (F : ℝ → ℝ) : Prop

Split version of the interior note-shaped raw estimate.

Equations

• HCPolySupport.CoarseCaccioppoliInteriorNoteRawEstimateSplit Q a s t Calpha Ccross uL2Sq h F = HCPolySupport.CoarseCaccioppoliBoundaryNoteRawEstimateSplit Q a s t Calpha Ccross uL2Sq h F

def HCPolySupport.CoarseCaccioppoliInteriorNoteCoefficientControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) : Prop

The interior note-shaped coefficient-control surface currently reuses the boundary one.

Equations

• HCPolySupport.CoarseCaccioppoliInteriorNoteCoefficientControl Q a s t C uL2Sq h = HCPolySupport.CoarseCaccioppoliBoundaryNoteCoefficientControl Q a s t C uL2Sq h

def HCPolySupport.CoarseCaccioppoliInteriorNoteAbsorptionCondition {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (h : ℝ → ℝ → ℝ) : Prop

The interior note-specific absorption condition currently matches the boundary one.

Equations

• HCPolySupport.CoarseCaccioppoliInteriorNoteAbsorptionCondition Q a s t C h = HCPolySupport.CoarseCaccioppoliBoundaryNoteAbsorptionCondition Q a s t C h

def HCPolySupport.CoarseCaccioppoliInteriorNoteCrossTermBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) : Prop

The interior note-specific cross-term bookkeeping condition currently matches the boundary one.

Equations

• HCPolySupport.CoarseCaccioppoliInteriorNoteCrossTermBound Q a s t C uL2Sq h = HCPolySupport.CoarseCaccioppoliBoundaryNoteCrossTermBound Q a s t C uL2Sq h

def HCPolySupport.CoarseCaccioppoliInteriorHeightChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (h : ℝ → ℝ → ℝ) : Prop

The interior note-facing explicit height choice currently reuses the boundary bookkeeping surface; the later distinction is only in how the local estimate is centered.

Equations

• HCPolySupport.CoarseCaccioppoliInteriorHeightChoice Q a s t C h = HCPolySupport.CoarseCaccioppoliBoundaryHeightChoice Q a s t C h