Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.EnergyBridge.LocalEstimate.Split

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

Local energy estimate: split exact RHS bridge

theorem HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_split_of_fluxEnergyControl_of_contDiff_component_bound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (flux : Vec d → Vec d) (u g : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) {Acirc1 AcircS B C BgConst BgCent : ℝ} (hB : 0 ≤ B) (hs0 : 0 < s) (hs1 : s < 1) (hfluxMem : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q)) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (hBgConst : 0 ≤ BgConst) (hBgCent : 0 ≤ BgCent) (hC : 0 ≤ C) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hfluxCtrl : CubeAverageFluxEnergyControl Q a flux energy) (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)) (hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g N) (hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i) (hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B) (hgCirc1 : ∀ (N : ℕ), cubeBesovCircPartialNorm Q 1 2 1 N g ≤ Acirc1 * √(cubeAverage Q energy)) (hgCircS : ∀ (N : ℕ), cubeBesovCircPartialNorm Q (1 - s) 2 1 N g ≤ AcircS * √(cubeAverage Q energy)) (hBgConst_bound : cubeLpNorm Q 2 u * (B + cubeBesovScaleWeight 1 Q * cubeLpNorm Q ⊤ ξ) ≤ BgConst) (hBgCent_bound : 2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * (Acirc1 * √(cubeAverage Q energy)))) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * (AcircS * √(cubeAverage Q energy))))) ≤ BgCent) : have E := √(cubeAverage Q energy); have Aavg := √(coarseBBlockNorm Q a); have Aflux1 := (geometricDiscount 1 1)⁻¹ * (LambdaSq Q 1 (MultiscaleExponent.finite 1) a).rpow (1 / 2); have AfluxS := (geometricDiscount s 1)⁻¹ * (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2); |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ ↑d * (3 ^ (↑d + 1) * (cubeBesovScaleWeight (-1) Q * (Aflux1 * E)) * BgConst) + (↑d * (Aavg * E * (cubeLpNorm Q ⊤ ξ * (3 / 2 * C * 3 ^ (↑d + 1) * (Acirc1 * E)))) + ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * (AfluxS * E)) * (cubeBesovScaleWeight s Q * BgCent)))

The split local Caccioppoli estimate with all flux-side Besov and average hypotheses supplied by the coarse-Poincare flux energy-control interface. The remaining hypotheses are exactly the scalar projected-Poincare/cutoff-product side and the elementary cutoff-size bounds.

theorem HCPolySupport.abs_cubeAverage_fluxCutoff_le_split_of_fluxEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (flux : Vec d → Vec d) (u : Vec d → ℝ) (G ξ : Vec d → Vec d) (energy : Vec d → ℝ) {Acirc1 AcircS B C BgConst BgCent : ℝ} (hB : 0 ≤ B) (hs0 : 0 < s) (hs1 : s < 1) (hfluxMem : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q)) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (hBgConst : 0 ≤ BgConst) (hBgCent : 0 ≤ BgCent) (hC : 0 ≤ C) (hAcircS : 0 ≤ AcircS) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hfluxCtrl : CubeAverageFluxEnergyControl Q a flux energy) (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)) (hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate Q C (cubeFluctuation Q u) G N) (hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i) (hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B) (hGcirc1 : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => G x i) ≤ Acirc1 * √(cubeAverage Q energy)) (hGcircS : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ AcircS * √(cubeAverage Q energy)) (hBgConst_bound : cubeLpNorm Q 2 u * (B + cubeBesovScaleWeight 1 Q * cubeLpNorm Q ⊤ ξ) ≤ BgConst) (hBgCent_bound : 2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * (↑(Fintype.card (Fin d)) * C) * 3 ^ (↑d + 1) * (Acirc1 * √(cubeAverage Q energy)))) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * (↑(Fintype.card (Fin d)) * C) * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * (AcircS * √(cubeAverage Q energy))))) ≤ BgCent) : have E := √(cubeAverage Q energy); have Aavg := √(coarseBBlockNorm Q a); have Aflux1 := (geometricDiscount 1 1)⁻¹ * (LambdaSq Q 1 (MultiscaleExponent.finite 1) a).rpow (1 / 2); have AfluxS := (geometricDiscount s 1)⁻¹ * (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2); |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ ↑d * (3 ^ (↑d + 1) * (cubeBesovScaleWeight (-1) Q * (Aflux1 * E)) * BgConst) + (↑d * (Aavg * E * (cubeLpNorm Q ⊤ ξ * (3 / 2 * (↑(Fintype.card (Fin d)) * C) * 3 ^ (↑d + 1) * (Acirc1 * E)))) + ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * (AfluxS * E)) * (cubeBesovScaleWeight s Q * BgCent)))

theorem HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_split_of_fluxEnergyControl_of_exact_cutoff_sizes {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (flux : Vec d → Vec d) (u g : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) {Acirc1 AcircS B C : ℝ} (hB : 0 ≤ B) (hs0 : 0 < s) (hs1 : s < 1) (hfluxMem : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q)) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (hBgConst : 0 ≤ coarseCaccioppoliConstantCutoffSize Q u ξ B) (hBgCent : 0 ≤ coarseCaccioppoliCenteredCutoffSize Q s ξ Acirc1 AcircS (√(cubeAverage Q energy)) B C) (hC : 0 ≤ C) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hfluxCtrl : CubeAverageFluxEnergyControl Q a flux energy) (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)) (hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g N) (hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i) (hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B) (hgCirc1 : ∀ (N : ℕ), cubeBesovCircPartialNorm Q 1 2 1 N g ≤ Acirc1 * √(cubeAverage Q energy)) (hgCircS : ∀ (N : ℕ), cubeBesovCircPartialNorm Q (1 - s) 2 1 N g ≤ AcircS * √(cubeAverage Q energy)) : have E := √(cubeAverage Q energy); have Aavg := √(coarseBBlockNorm Q a); have Aflux1 := (geometricDiscount 1 1)⁻¹ * (LambdaSq Q 1 (MultiscaleExponent.finite 1) a).rpow (1 / 2); have AfluxS := (geometricDiscount s 1)⁻¹ * (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2); have BgConst := coarseCaccioppoliConstantCutoffSize Q u ξ B; have BgCent := coarseCaccioppoliCenteredCutoffSize Q s ξ Acirc1 AcircS E B C; |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ ↑d * (3 ^ (↑d + 1) * (cubeBesovScaleWeight (-1) Q * (Aflux1 * E)) * BgConst) + (↑d * (Aavg * E * (cubeLpNorm Q ⊤ ξ * (3 / 2 * C * 3 ^ (↑d + 1) * (Acirc1 * E)))) + ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * (AfluxS * E)) * (cubeBesovScaleWeight s Q * BgCent)))

Version of the flux-energy bridge using the exact cutoff sizes instead of separate upper-bound hypotheses for BgConst and BgCent.

This is the last purely local bookkeeping step before the note-facing single-cube estimate: the remaining work is to dominate these exact cutoff sizes by the Chapter-3 radius/height coefficients.

theorem HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_split_of_fluxEnergyControls_of_scalarCutoffControls {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (flux : Vec d → Vec d) (u g : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) {Acirc1 AcircS B C : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hfluxMem : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q)) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (hfluxEnergy : CoarseCaccioppoliFluxEnergyControls Q a s flux energy) (hscalar : CoarseCaccioppoliScalarCutoffControls Q s u g ξ energy Acirc1 AcircS B C) : have E := √(cubeAverage Q energy); have Aavg := √(coarseBBlockNorm Q a); have Aflux1 := (geometricDiscount 1 1)⁻¹ * (LambdaSq Q 1 (MultiscaleExponent.finite 1) a).rpow (1 / 2); have AfluxS := (geometricDiscount s 1)⁻¹ * (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2); have BgConst := coarseCaccioppoliConstantCutoffSize Q u ξ B; have BgCent := coarseCaccioppoliCenteredCutoffSize Q s ξ Acirc1 AcircS E B C; |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ ↑d * (3 ^ (↑d + 1) * (cubeBesovScaleWeight (-1) Q * (Aflux1 * E)) * BgConst) + (↑d * (Aavg * E * (cubeLpNorm Q ⊤ ξ * (3 / 2 * C * 3 ^ (↑d + 1) * (Acirc1 * E)))) + ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * (AfluxS * E)) * (cubeBesovScaleWeight s Q * BgCent)))

Bundled-hypothesis version of the flux-energy/exact-cutoff bridge.

theorem HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_fluxEnergyExactRhs_of_controls {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (flux : Vec d → Vec d) (u g : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) {Acirc1 AcircS B C : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hfluxMem : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q)) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (hfluxEnergy : CoarseCaccioppoliFluxEnergyControls Q a s flux energy) (hscalar : CoarseCaccioppoliScalarCutoffControls Q s u g ξ energy Acirc1 AcircS B C) : |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ coarseCaccioppoliFluxEnergyExactRhs Q a s u ξ energy Acirc1 AcircS B C

Compact exact-RHS form of the local coarse Caccioppoli bridge.

theorem HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_fluxEnergyExactRhs_of_vectorControls {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (flux : Vec d → Vec d) (u : Vec d → ℝ) (G ξ : Vec d → Vec d) (energy : Vec d → ℝ) {Acirc1 AcircS B C : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (hfluxMem : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q)) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (hfluxEnergy : CoarseCaccioppoliFluxEnergyControls Q a s flux energy) (hvector : CoarseCaccioppoliVectorCutoffControls Q s u G ξ energy Acirc1 AcircS B C) : |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ coarseCaccioppoliFluxEnergyExactRhs Q a s u ξ energy Acirc1 AcircS B (↑(Fintype.card (Fin d)) * C)

Compact exact-RHS form of the local coarse Caccioppoli bridge, using the vector projected-Poincare package. The scalar-facing exact RHS receives the effective constant (Fintype.card (Fin d) : ℝ) * C.