Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.EnergyBridge.ExactRhs

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

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

The exact local RHS produced after substituting flux-side energy controls and the scalar/cutoff control bundle into the split Caccioppoli pairing.

The next coefficient-bookkeeping theorem should prove this quantity is bounded by the note's single-cube RHS.

Equations

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

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactRhs_congr_cubeAverage {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → ℝ) (ξ : Vec d → Vec d) {energy₁ energy₂ : Vec d → ℝ} (Acirc1 AcircS B C : ℝ) (havg : cubeAverage Q energy₁ = cubeAverage Q energy₂) : coarseCaccioppoliFluxEnergyExactRhs Q a s u ξ energy₁ Acirc1 AcircS B C = coarseCaccioppoliFluxEnergyExactRhs Q a s u ξ energy₂ Acirc1 AcircS B C

The exact local RHS only sees the energy density through its cube average.

noncomputable def HCPolySupport.coarseCaccioppoliFluxEnergyExactConstantRhs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) (B : ℝ) : ℝ

Constant-piece summand of coarseCaccioppoliFluxEnergyExactRhs.

Equations

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

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactConstantRhs_congr_cubeAverage {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → ℝ) (ξ : Vec d → Vec d) {energy₁ energy₂ : Vec d → ℝ} (B : ℝ) (havg : cubeAverage Q energy₁ = cubeAverage Q energy₂) : coarseCaccioppoliFluxEnergyExactConstantRhs Q a u ξ energy₁ B = coarseCaccioppoliFluxEnergyExactConstantRhs Q a u ξ energy₂ B

The exact constant-piece RHS only sees the energy density through its cube average.

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

Coefficient in the exact constant-piece RHS, after factoring out the energy norm and cutoff size.

Equations

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

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactConstantCoeff_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) : 0 ≤ coarseCaccioppoliFluxEnergyExactConstantCoeff Q a

noncomputable def HCPolySupport.coarseCaccioppoliFluxEnergyExactConstantCoeffFactorBound {d : ℕ} (Q : TriadicCube d) (_Aavg Aflux1 : ℝ) : ℝ

Separated factor-bound expression for the exact constant flux coefficient. Aavg bounds the block-average coefficient and Aflux1 bounds the finite q = 1 flux Besov coefficient.

Equations

• HCPolySupport.coarseCaccioppoliFluxEnergyExactConstantCoeffFactorBound Q _Aavg Aflux1 = ↑d * (3 ^ (↑d + 1) * (HCPolySupport.cubeBesovScaleWeight (-1) Q * Aflux1))

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactConstantCoeffFactorBound_nonneg {d : ℕ} (Q : TriadicCube d) {Aavg Aflux1 : ℝ} (_hAavg : 0 ≤ Aavg) (hAflux1 : 0 ≤ Aflux1) : 0 ≤ coarseCaccioppoliFluxEnergyExactConstantCoeffFactorBound Q Aavg Aflux1

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactConstantCoeff_le_factorBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {Aavg Aflux1 : ℝ} (_hAavg : √(coarseBBlockNorm Q a) ≤ Aavg) (hAflux1 : (geometricDiscount 1 1)⁻¹ * (LambdaSq Q 1 (MultiscaleExponent.finite 1) a).rpow (1 / 2) ≤ Aflux1) : coarseCaccioppoliFluxEnergyExactConstantCoeff Q a ≤ coarseCaccioppoliFluxEnergyExactConstantCoeffFactorBound Q Aavg Aflux1

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactConstantRhs_eq_coeff_mul {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) (B : ℝ) : coarseCaccioppoliFluxEnergyExactConstantRhs Q a u ξ energy B = coarseCaccioppoliFluxEnergyExactConstantCoeff Q a * coarseCaccioppoliConstantCutoffSize Q u ξ B * √(cubeAverage Q energy)

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactConstantRhs_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) {B : ℝ} (hB : 0 ≤ B) : 0 ≤ coarseCaccioppoliFluxEnergyExactConstantRhs Q a u ξ energy B

noncomputable def HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredRhs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) (Acirc1 AcircS B C : ℝ) : ℝ

Centered-piece summand of coarseCaccioppoliFluxEnergyExactRhs.

Equations

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

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredRhs_congr_cubeAverage {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (ξ : Vec d → Vec d) {energy₁ energy₂ : Vec d → ℝ} (Acirc1 AcircS B C : ℝ) (havg : cubeAverage Q energy₁ = cubeAverage Q energy₂) : coarseCaccioppoliFluxEnergyExactCenteredRhs Q a s ξ energy₁ Acirc1 AcircS B C = coarseCaccioppoliFluxEnergyExactCenteredRhs Q a s ξ energy₂ Acirc1 AcircS B C

The exact centered-piece RHS only sees the energy density through its cube average.

noncomputable def HCPolySupport.coarseCaccioppoliCenteredCutoffCoeff {d : ℕ} (Q : TriadicCube d) (s : ℝ) (ξ : Vec d → Vec d) (Acirc1 AcircS B C : ℝ) : ℝ

Centered cutoff coefficient after factoring out the energy norm.

Equations

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

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

Coefficient in the exact centered-piece RHS after factoring out (sqrt energy)^2.

Equations

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

noncomputable def HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredAverageCoeff {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (ξ : Vec d → Vec d) (Acirc1 C : ℝ) : ℝ

Average-flux part of the exact centered coefficient.

Equations

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

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

Besov/cutoff-product part of the exact centered coefficient.

Equations

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

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredCoeff_eq_average_add_besov {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (ξ : Vec d → Vec d) (Acirc1 AcircS B C : ℝ) : coarseCaccioppoliFluxEnergyExactCenteredCoeff Q a s ξ Acirc1 AcircS B C = coarseCaccioppoliFluxEnergyExactCenteredAverageCoeff Q a ξ Acirc1 C + coarseCaccioppoliFluxEnergyExactCenteredBesovCoeff Q a s ξ Acirc1 AcircS B C

theorem HCPolySupport.coarseCaccioppoliCenteredCutoffCoeff_nonneg {d : ℕ} (Q : TriadicCube d) {s : ℝ} (ξ : Vec d → Vec d) {Acirc1 AcircS B C : ℝ} (hs : 0 < s) (hAcirc1 : 0 ≤ Acirc1) (hAcircS : 0 ≤ AcircS) (hB : 0 ≤ B) (hC : 0 ≤ C) : 0 ≤ coarseCaccioppoliCenteredCutoffCoeff Q s ξ Acirc1 AcircS B C

noncomputable def HCPolySupport.coarseCaccioppoliCenteredCutoffCoeffFactorBound {d : ℕ} (Q : TriadicCube d) (s Xi D A1 AS C : ℝ) : ℝ

Separated factor-bound expression for the centered cutoff coefficient. Xi bounds ‖ξ‖_{L∞}, D bounds ‖∇ξ‖_{L∞}, and A1, AS bound the two projected Poincare/Besov scalar constants.

Equations

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

theorem HCPolySupport.cubeBesovScaleWeight_mul_centeredCutoffCoeffFactorBound_eq {d : ℕ} (Q : TriadicCube d) (s Xi D A1 AS C : ℝ) : cubeBesovScaleWeight s Q * coarseCaccioppoliCenteredCutoffCoeffFactorBound Q s Xi D A1 AS C = 2 * (cubeBesovScaleWeight s Q * (cubeScaleFactor Q * D * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * A1))) + Xi * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * AS))

Multiplying the centered cutoff factor by the descendant Besov weight cancels the cubeBesovScaleWeight (-s) in the A_s^\circ term.

theorem HCPolySupport.coarseCaccioppoliCenteredCutoffCoeffFactorBound_nonneg {d : ℕ} (Q : TriadicCube d) {s Xi D A1 AS C : ℝ} (hs : 0 < s) (hXi : 0 ≤ Xi) (hD : 0 ≤ D) (hA1 : 0 ≤ A1) (hAS : 0 ≤ AS) (hC : 0 ≤ C) : 0 ≤ coarseCaccioppoliCenteredCutoffCoeffFactorBound Q s Xi D A1 AS C

theorem HCPolySupport.coarseCaccioppoliCenteredCutoffCoeff_le_factorBound {d : ℕ} (Q : TriadicCube d) {s : ℝ} (ξ : Vec d → Vec d) {Acirc1 AcircS B C Xi D A1 AS : ℝ} (hs : 0 < s) (hAcirc1_nonneg : 0 ≤ Acirc1) (hAcircS_nonneg : 0 ≤ AcircS) (hXi_nonneg : 0 ≤ Xi) (hD_nonneg : 0 ≤ D) (hC : 0 ≤ C) (hξ : cubeLpNorm Q ⊤ ξ ≤ Xi) (hB : B ≤ D) (hAcirc1 : Acirc1 ≤ A1) (hAcircS : AcircS ≤ AS) : coarseCaccioppoliCenteredCutoffCoeff Q s ξ Acirc1 AcircS B C ≤ coarseCaccioppoliCenteredCutoffCoeffFactorBound Q s Xi D A1 AS C

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredAverageCoeff_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (ξ : Vec d → Vec d) {Acirc1 C : ℝ} (hAcirc1 : 0 ≤ Acirc1) (hC : 0 ≤ C) : 0 ≤ coarseCaccioppoliFluxEnergyExactCenteredAverageCoeff Q a ξ Acirc1 C

noncomputable def HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound {d : ℕ} (Aavg Xi A1 C : ℝ) : ℝ

Separated factor-bound expression for the average-flux part of the centered coefficient.

Equations

• HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound Aavg Xi A1 C = ↑d * (Aavg * (Xi * (3 / 2 * C * 3 ^ (↑d + 1) * A1)))

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound_nonneg {d : ℕ} {Aavg Xi A1 C : ℝ} (hAavg : 0 ≤ Aavg) (hXi : 0 ≤ Xi) (hA1 : 0 ≤ A1) (hC : 0 ≤ C) : 0 ≤ coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound Aavg Xi A1 C

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredAverageCoeff_le_factorBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (ξ : Vec d → Vec d) {Acirc1 C Aavg Xi A1 : ℝ} (hAavg_nonneg : 0 ≤ Aavg) (hXi_nonneg : 0 ≤ Xi) (hAcirc1_nonneg : 0 ≤ Acirc1) (hC : 0 ≤ C) (hAavg : √(coarseBBlockNorm Q a) ≤ Aavg) (hξ : cubeLpNorm Q ⊤ ξ ≤ Xi) (hAcirc1 : Acirc1 ≤ A1) : coarseCaccioppoliFluxEnergyExactCenteredAverageCoeff Q a ξ Acirc1 C ≤ coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound Aavg Xi A1 C

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredBesovCoeff_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (ξ : Vec d → Vec d) {Acirc1 AcircS B C : ℝ} (hs : 0 < s) (hAcirc1 : 0 ≤ Acirc1) (hAcircS : 0 ≤ AcircS) (hB : 0 ≤ B) (hC : 0 ≤ C) : 0 ≤ coarseCaccioppoliFluxEnergyExactCenteredBesovCoeff Q a s ξ Acirc1 AcircS B C

noncomputable def HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound {d : ℕ} (Q : TriadicCube d) (s _Aavg AfluxS BgCent : ℝ) : ℝ

Separated factor-bound expression for the Besov/cutoff-product part of the centered coefficient.

Equations

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

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound_nonneg {d : ℕ} (Q : TriadicCube d) {s Aavg AfluxS BgCent : ℝ} (_hAavg : 0 ≤ Aavg) (hAfluxS : 0 ≤ AfluxS) (hBgCent : 0 ≤ BgCent) : 0 ≤ coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound Q s Aavg AfluxS BgCent

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredBesovCoeff_le_factorBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (ξ : Vec d → Vec d) {Acirc1 AcircS B C Aavg AfluxS BgCent : ℝ} (_hAavg_nonneg : 0 ≤ Aavg) (hAfluxS_nonneg : 0 ≤ AfluxS) (hBgCentCoeff_nonneg : 0 ≤ coarseCaccioppoliCenteredCutoffCoeff Q s ξ Acirc1 AcircS B C) (_hAavg : √(coarseBBlockNorm Q a) ≤ Aavg) (hAfluxS : (geometricDiscount s 1)⁻¹ * (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2) ≤ AfluxS) (hBgCent : coarseCaccioppoliCenteredCutoffCoeff Q s ξ Acirc1 AcircS B C ≤ BgCent) : coarseCaccioppoliFluxEnergyExactCenteredBesovCoeff Q a s ξ Acirc1 AcircS B C ≤ coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound Q s Aavg AfluxS BgCent

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredCoeff_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (ξ : Vec d → Vec d) {Acirc1 AcircS B C : ℝ} (hs : 0 < s) (hAcirc1 : 0 ≤ Acirc1) (hAcircS : 0 ≤ AcircS) (hB : 0 ≤ B) (hC : 0 ≤ C) : 0 ≤ coarseCaccioppoliFluxEnergyExactCenteredCoeff Q a s ξ Acirc1 AcircS B C

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredCoeff_mono_Acirc {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (ξ : Vec d → Vec d) {Acirc1 AcircS A1 AS B C : ℝ} (hs : 0 < s) (hC : 0 ≤ C) (hB : 0 ≤ B) (hAcirc1_nonneg : 0 ≤ Acirc1) (hAcircS_nonneg : 0 ≤ AcircS) (hA1 : Acirc1 ≤ A1) (hAS : AcircS ≤ AS) : coarseCaccioppoliFluxEnergyExactCenteredCoeff Q a s ξ Acirc1 AcircS B C ≤ coarseCaccioppoliFluxEnergyExactCenteredCoeff Q a s ξ A1 AS B C

The exact centered coefficient is monotone in the two canonical gradient slots. This is the local-to-parent A^\circ comparison used in the small-cube Caccioppoli proof.

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredRhs_eq_coeff_mul_sqrt_sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) (Acirc1 AcircS B C : ℝ) : coarseCaccioppoliFluxEnergyExactCenteredRhs Q a s ξ energy Acirc1 AcircS B C = coarseCaccioppoliFluxEnergyExactCenteredCoeff Q a s ξ Acirc1 AcircS B C * (√(cubeAverage Q energy) * √(cubeAverage Q energy))

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredRhs_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (ξ : Vec d → Vec d) (energy : Vec d → ℝ) {Acirc1 AcircS B C : ℝ} (hs : 0 < s) (hAcirc1 : 0 ≤ Acirc1) (hAcircS : 0 ≤ AcircS) (hB : 0 ≤ B) (hC : 0 ≤ C) : 0 ≤ coarseCaccioppoliFluxEnergyExactCenteredRhs Q a s ξ energy Acirc1 AcircS B C

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactRhs_eq_constant_add_centered {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) (Acirc1 AcircS B C : ℝ) : coarseCaccioppoliFluxEnergyExactRhs Q a s u ξ energy Acirc1 AcircS B C = coarseCaccioppoliFluxEnergyExactConstantRhs Q a u ξ energy B + coarseCaccioppoliFluxEnergyExactCenteredRhs Q a s ξ energy Acirc1 AcircS B C

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactRhs_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (u : Vec d → ℝ) (ξ : Vec d → Vec d) (energy : Vec d → ℝ) {Acirc1 AcircS B C : ℝ} (hs : 0 < s) (hAcirc1 : 0 ≤ Acirc1) (hAcircS : 0 ≤ AcircS) (hB : 0 ≤ B) (hC : 0 ≤ C) : 0 ≤ coarseCaccioppoliFluxEnergyExactRhs Q a s u ξ energy Acirc1 AcircS B C