Documentation

Note-facing single-cube boundary Caccioppoli RHS.

The parameters k and h are the triadic gap scale and auxiliary height from Chapter 3. The scalar energyAvg represents ‖σ^{1/2}∇u‖_{\underline L^2(Q)}^2, so its square root is the normalized energy norm appearing in the first term.

Equations

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

Instances For

noncomputable def HCPolySupport.coarseCaccioppoliSingleCubeBoundaryConstantRhs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (C k uL2Sq energyAvg : ℝ) :

Constant-piece summand of coarseCaccioppoliSingleCubeBoundaryNoteRhs.

Equations

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

Instances For

noncomputable def HCPolySupport.coarseCaccioppoliSingleCubeBoundaryConstantCoeff {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (C k uL2Sq : ℝ) :

Coefficient in the note's constant-piece RHS, after factoring out the energy norm.

Equations

HCPolySupport.coarseCaccioppoliSingleCubeBoundaryConstantCoeff Q a C k uL2Sq = C * Real.rpow 3 k * (HCPolySupport.LambdaSq Q 1 (HCPolySupport.MultiscaleExponent.finite 1) a).rpow (1 / 2) * √uL2Sq

Instances For

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

The constant-piece single-cube coefficient before multiplying by the global L² size of u.

This is the coefficient used in the small-cube summation proof: the local estimate keeps the local L² norm of u, and the descendant average is collapsed by finite Cauchy only after summing over the small cubes.

Equations

HCPolySupport.coarseCaccioppoliSingleCubeBoundaryConstantBaseCoeff Q a C k = C * Real.rpow 3 k * (HCPolySupport.LambdaSq Q 1 (HCPolySupport.MultiscaleExponent.finite 1) a).rpow (1 / 2)

Instances For

theorem HCPolySupport.coarseCaccioppoliSingleCubeBoundaryConstantCoeff_eq_baseCoeff_mul_sqrt {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (C k uL2Sq : ℝ) :

coarseCaccioppoliSingleCubeBoundaryConstantCoeff Q a C k uL2Sq = coarseCaccioppoliSingleCubeBoundaryConstantBaseCoeff Q a C k * √uL2Sq

theorem HCPolySupport.coarseCaccioppoliSingleCubeBoundaryConstantBaseCoeff_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {C k : ℝ} (hC : 0 ≤ C) :

0 ≤ coarseCaccioppoliSingleCubeBoundaryConstantBaseCoeff Q a C k

theorem HCPolySupport.coarseCaccioppoliSingleCubeBoundaryConstantBaseCoeff_mono_scale {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {C k k' : ℝ} (hC : 0 ≤ C) (hk : k ≤ k') :

coarseCaccioppoliSingleCubeBoundaryConstantBaseCoeff Q a C k ≤ coarseCaccioppoliSingleCubeBoundaryConstantBaseCoeff Q a C k'

The constant base coefficient is monotone increasing in the scale parameter k.

theorem HCPolySupport.coarseCaccioppoliSingleCubeBoundaryConstantCoeff_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {C k uL2Sq : ℝ} (hC : 0 ≤ C) :

0 ≤ coarseCaccioppoliSingleCubeBoundaryConstantCoeff Q a C k uL2Sq

theorem HCPolySupport.coarseCaccioppoliSingleCubeBoundaryConstantCoeff_mono_scale {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {C k k' uL2Sq : ℝ} (hC : 0 ≤ C) (hk : k ≤ k') :

coarseCaccioppoliSingleCubeBoundaryConstantCoeff Q a C k uL2Sq ≤ coarseCaccioppoliSingleCubeBoundaryConstantCoeff Q a C k' uL2Sq

The constant coefficient after inserting the global L² size is monotone in the scale parameter k.

theorem HCPolySupport.coarseCaccioppoliSingleCubeBoundaryConstantRhs_eq_coeff_mul {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (C k uL2Sq energyAvg : ℝ) :

coarseCaccioppoliSingleCubeBoundaryConstantRhs Q a C k uL2Sq energyAvg = coarseCaccioppoliSingleCubeBoundaryConstantCoeff Q a C k uL2Sq * √energyAvg

noncomputable def HCPolySupport.coarseCaccioppoliSingleCubeBoundaryCenteredRhs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C k h energyAvg : ℝ) :

Centered-piece summand of coarseCaccioppoliSingleCubeBoundaryNoteRhs.

Equations

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

Instances For

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

Coefficient in the note's centered-piece RHS after factoring out energyAvg.

Equations

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

Instances For

theorem HCPolySupport.coarseCaccioppoliSingleCubeBoundaryCenteredCoeff_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s C k h : ℝ} (hC : 0 ≤ C) (hs0 : 0 < s) (hs1 : s < 1) :

0 ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff Q a s C k h

theorem HCPolySupport.coarseCaccioppoliSingleCubeBoundaryCenteredCoeff_mono_scale {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s C k k' h : ℝ} (hC : 0 ≤ C) (hs0 : 0 < s) (hs1 : s < 1) (hk : k ≤ k') :

coarseCaccioppoliSingleCubeBoundaryCenteredCoeff Q a s C k h ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff Q a s C k' h

The centered coefficient is monotone increasing in the scale parameter k.

theorem HCPolySupport.coarseCaccioppoliSingleCubeBoundaryCenteredCoeff_anti_mono_height {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s C k h h' : ℝ} (hC : 0 ≤ C) (hs0 : 0 < s) (hs1 : s < 1) (hh : h ≤ h') :

coarseCaccioppoliSingleCubeBoundaryCenteredCoeff Q a s C k h' ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff Q a s C k h

The centered single-cube coefficient is monotone decreasing in the auxiliary height.

theorem HCPolySupport.coarseCaccioppoliSingleCubeBoundaryCenteredRhs_eq_coeff_mul {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C k h energyAvg : ℝ) :

coarseCaccioppoliSingleCubeBoundaryCenteredRhs Q a s C k h energyAvg = coarseCaccioppoliSingleCubeBoundaryCenteredCoeff Q a s C k h * energyAvg

theorem HCPolySupport.coarseCaccioppoliSingleCubeBoundaryNoteRhs_eq_constant_add_centered {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C k h uL2Sq energyAvg : ℝ) :

coarseCaccioppoliSingleCubeBoundaryNoteRhs Q a s C k h uL2Sq energyAvg = coarseCaccioppoliSingleCubeBoundaryConstantRhs Q a C k uL2Sq energyAvg + coarseCaccioppoliSingleCubeBoundaryCenteredRhs Q a s C k h energyAvg

theorem HCPolySupport.coarseCaccioppoliSingleCubeBoundaryNoteRhs_mono_scale {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s C k k' h uL2Sq energyAvg : ℝ} (hC : 0 ≤ C) (hs0 : 0 < s) (hs1 : s < 1) (hk : k ≤ k') (henergy : 0 ≤ energyAvg) :

coarseCaccioppoliSingleCubeBoundaryNoteRhs Q a s C k h uL2Sq energyAvg ≤ coarseCaccioppoliSingleCubeBoundaryNoteRhs Q a s C k' h uL2Sq energyAvg

The note-facing single-cube RHS is monotone increasing in the outer scale parameter k.

def HCPolySupport.CoarseCaccioppoliSingleCubeCoefficientDomination {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C k h uL2Sq : ℝ) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) (Acirc1 AcircS B : ℝ) :

The coefficient-bookkeeping obligation left after the exact local cutoff/Besov bridge: dominate the exact local RHS by the note's single-cube RHS.

Equations

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

Instances For

theorem HCPolySupport.CoarseCaccioppoliSingleCubeCoefficientDomination.of_termwise {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C k h uL2Sq : ℝ) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) (Acirc1 AcircS B : ℝ) (hconst : coarseCaccioppoliFluxEnergyExactConstantRhs Q a u ξ energy B ≤ coarseCaccioppoliSingleCubeBoundaryConstantRhs Q a C k uL2Sq (cubeAverage Q energy)) (hcent : coarseCaccioppoliFluxEnergyExactCenteredRhs Q a s ξ energy Acirc1 AcircS B C ≤ coarseCaccioppoliSingleCubeBoundaryCenteredRhs Q a s C k h (cubeAverage Q energy)) :

CoarseCaccioppoliSingleCubeCoefficientDomination Q a s C k h uL2Sq u ξ energy Acirc1 AcircS B

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactConstantRhs_le_singleCubeBoundaryConstantRhs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) (B C k uL2Sq : ℝ) (hcoeff : coarseCaccioppoliFluxEnergyExactConstantCoeff Q a * coarseCaccioppoliConstantCutoffSize Q u ξ B ≤ coarseCaccioppoliSingleCubeBoundaryConstantCoeff Q a C k uL2Sq) :

coarseCaccioppoliFluxEnergyExactConstantRhs Q a u ξ energy B ≤ coarseCaccioppoliSingleCubeBoundaryConstantRhs Q a C k uL2Sq (cubeAverage Q energy)

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredRhs_le_singleCubeBoundaryCenteredRhs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) (Acirc1 AcircS B C k h : ℝ) (henergy : 0 ≤ cubeAverage Q energy) (hcoeff : coarseCaccioppoliFluxEnergyExactCenteredCoeff Q a s ξ Acirc1 AcircS B C ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff Q a s C k h) :

coarseCaccioppoliFluxEnergyExactCenteredRhs Q a s ξ energy Acirc1 AcircS B C ≤ coarseCaccioppoliSingleCubeBoundaryCenteredRhs Q a s C k h (cubeAverage Q energy)

def HCPolySupport.CoarseCaccioppoliConstantCoefficientDomination {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (C k uL2Sq : ℝ) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (B : ℝ) :

Coefficient-only domination for the constant part of the exact local RHS.

Equations

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

Instances For

theorem HCPolySupport.CoarseCaccioppoliConstantCoefficientDomination.of_factor_bounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (C k uL2Sq : ℝ) (u : Vec d → ℝ) (ξ : Vec d → Vec d) {B A G : ℝ} (hA_nonneg : 0 ≤ A) (hB : 0 ≤ B) (hcoeff : coarseCaccioppoliFluxEnergyExactConstantCoeff Q a ≤ A) (hcutoff : coarseCaccioppoliConstantCutoffSize Q u ξ B ≤ G) (hAG : A * G ≤ coarseCaccioppoliSingleCubeBoundaryConstantCoeff Q a C k uL2Sq) :

CoarseCaccioppoliConstantCoefficientDomination Q a C k uL2Sq u ξ B

Prove constant-piece coefficient domination from separate bounds on the flux coefficient and cutoff size.

def HCPolySupport.CoarseCaccioppoliCenteredCoefficientDomination {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C k h : ℝ) (ξ : Vec d → Vec d) (Acirc1 AcircS B : ℝ) :

Coefficient-only domination for the centered part of the exact local RHS.

Equations

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

Instances For

theorem HCPolySupport.CoarseCaccioppoliCenteredCoefficientDomination.of_termwise {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C k h : ℝ) (ξ : Vec d → Vec d) (Acirc1 AcircS B : ℝ) {X Y : ℝ} (havg : coarseCaccioppoliFluxEnergyExactCenteredAverageCoeff Q a ξ Acirc1 C ≤ X) (hbesov : coarseCaccioppoliFluxEnergyExactCenteredBesovCoeff Q a s ξ Acirc1 AcircS B C ≤ Y) (hXY : X + Y ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff Q a s C k h) :

CoarseCaccioppoliCenteredCoefficientDomination Q a s C k h ξ Acirc1 AcircS B

Prove centered-piece coefficient domination by bounding the average-flux and Besov/cutoff-product parts separately.

def HCPolySupport.CoarseCaccioppoliSingleCubeCoefficientControls {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C k h uL2Sq : ℝ) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (Acirc1 AcircS B : ℝ) :

The two coefficient inequalities left after the exact cutoff/Besov local bridge has been factored into constant and centered pieces.

Equations

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

Instances For

theorem HCPolySupport.CoarseCaccioppoliSingleCubeCoefficientControls.of_factor_bounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C k h uL2Sq : ℝ) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (Acirc1 AcircS : ℝ) {B A G X Y : ℝ} (hA_nonneg : 0 ≤ A) (hB : 0 ≤ B) (hconstCoeff : coarseCaccioppoliFluxEnergyExactConstantCoeff Q a ≤ A) (hconstCutoff : coarseCaccioppoliConstantCutoffSize Q u ξ B ≤ G) (hconst : A * G ≤ coarseCaccioppoliSingleCubeBoundaryConstantCoeff Q a C k uL2Sq) (havg : coarseCaccioppoliFluxEnergyExactCenteredAverageCoeff Q a ξ Acirc1 C ≤ X) (hbesov : coarseCaccioppoliFluxEnergyExactCenteredBesovCoeff Q a s ξ Acirc1 AcircS B C ≤ Y) (hcentered : X + Y ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff Q a s C k h) :

CoarseCaccioppoliSingleCubeCoefficientControls Q a s C k h uL2Sq u ξ Acirc1 AcircS B

Build the bundled coefficient controls from the separated constant cutoff-size estimate and the centered average/Besov estimates.

theorem HCPolySupport.CoarseCaccioppoliSingleCubeCoefficientControls.of_separated_factor_bounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C k h uL2Sq : ℝ) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (Acirc1 AcircS : ℝ) {B AavgConst AavgCent Aflux1 AfluxS U Xi D A1 AS : ℝ} (hs0 : 0 < s) (hC : 0 ≤ C) (hB_nonneg : 0 ≤ B) (hAcirc1_nonneg : 0 ≤ Acirc1) (hAcircS_nonneg : 0 ≤ AcircS) (hAavgConst : √(coarseBBlockNorm Q a) ≤ AavgConst) (hAavgCent : √(coarseBBlockNorm Q a) ≤ AavgCent) (hAflux1 : (geometricDiscount 1 1)⁻¹ * (LambdaSq Q 1 (MultiscaleExponent.finite 1) a).rpow (1 / 2) ≤ Aflux1) (hAfluxS : (geometricDiscount s 1)⁻¹ * (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2) ≤ AfluxS) (hu : cubeLpNorm Q 2 u ≤ U) (hξ : cubeLpNorm Q ⊤ ξ ≤ Xi) (hB : B ≤ D) (hAcirc1 : Acirc1 ≤ A1) (hAcircS : AcircS ≤ AS) (hconst : coarseCaccioppoliFluxEnergyExactConstantCoeffFactorBound Q AavgConst Aflux1 * coarseCaccioppoliConstantCutoffSizeFactorBound Q U Xi D ≤ coarseCaccioppoliSingleCubeBoundaryConstantCoeff Q a C k uL2Sq) (hcentered : coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound AavgCent Xi A1 C + coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound Q s AavgCent AfluxS (coarseCaccioppoliCenteredCutoffCoeffFactorBound Q s Xi D A1 AS C) ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff Q a s C k h) :

CoarseCaccioppoliSingleCubeCoefficientControls Q a s C k h uL2Sq u ξ Acirc1 AcircS B

Build the coefficient controls from primitive scalar factor estimates: bounds for ‖u‖₂, ‖ξ‖∞, ‖∇ξ‖∞, the scalar projected-Poincare factors, and the average/flux coefficient factors. This is the final algebraic layer before a concrete cutoff construction supplies those scalar estimates.

theorem HCPolySupport.CoarseCaccioppoliSingleCubeCoefficientControls.of_canonical_factor_bounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C k h uL2Sq : ℝ) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (Acirc1 AcircS : ℝ) {B U Xi D A1 AS : ℝ} (hs0 : 0 < s) (hC : 0 ≤ C) (hsum1 : Summable fun (n : ℕ) => geometricWeight 1 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hsumS : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hB_nonneg : 0 ≤ B) (hAcirc1_nonneg : 0 ≤ Acirc1) (hAcircS_nonneg : 0 ≤ AcircS) (hu : cubeLpNorm Q 2 u ≤ U) (hξ : cubeLpNorm Q ⊤ ξ ≤ Xi) (hB : B ≤ D) (hAcirc1 : Acirc1 ≤ A1) (hAcircS : AcircS ≤ AS) (hconst : coarseCaccioppoliFluxEnergyExactConstantCoeffFactorBound Q (coarseCaccioppoliLambdaFactor Q a 1) (coarseCaccioppoliLambdaFactor Q a 1) * coarseCaccioppoliConstantCutoffSizeFactorBound Q U Xi D ≤ coarseCaccioppoliSingleCubeBoundaryConstantCoeff Q a C k uL2Sq) (hcentered : coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound (coarseCaccioppoliLambdaFactor Q a s) Xi A1 C + coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound Q s (coarseCaccioppoliLambdaFactor Q a s) (coarseCaccioppoliLambdaFactor Q a s) (coarseCaccioppoliCenteredCutoffCoeffFactorBound Q s Xi D A1 AS C) ≤ coarseCaccioppoliSingleCubeBoundaryCenteredCoeff Q a s C k h) :

CoarseCaccioppoliSingleCubeCoefficientControls Q a s C k h uL2Sq u ξ Acirc1 AcircS B

Canonical-factor version of the primitive coefficient-control constructor. The average and flux coefficient slots are filled by coarseCaccioppoliLambdaFactor; the two summability hypotheses are exactly the flux-energy inputs that justify the average-coefficient bounds.

theorem HCPolySupport.CoarseCaccioppoliSingleCubeCoefficientDomination.of_coefficientControls {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C k h uL2Sq : ℝ) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) (Acirc1 AcircS B : ℝ) (henergy : 0 ≤ cubeAverage Q energy) (hcoeff : CoarseCaccioppoliSingleCubeCoefficientControls Q a s C k h uL2Sq u ξ Acirc1 AcircS B) :

CoarseCaccioppoliSingleCubeCoefficientDomination Q a s C k h uL2Sq u ξ energy Acirc1 AcircS B