Coarse-graining support: Support.Deterministic.WeakFluxRHS.CorrectorEnergy

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

theorem HCPolySupport.MeanZeroNeumannCorrectorData.sq_cubeBesovNegativeVectorPartialSeminormTwo_corrector_le_two_mul_add {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) {u : Vec d → Vec d} (w : AHarmonicFunction a (cubeSet Q)) (huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) (hu : MemVectorL2 (cubeSet Q) u) (s : ℝ) (N : ℕ) : (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ^ 2 ≤ 2 * cubeBesovNegativeVectorPartialSeminormTwo Q s N u ^ 2 + 2 * (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x) ^ 2

theorem HCPolySupport.MeanZeroNeumannCorrectorData.cubeBesovNegativeVectorPartialSeminormTwo_corrector_le_sqrtTwo_mul_add {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) {u : Vec d → Vec d} (w : AHarmonicFunction a (cubeSet Q)) (huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) (hu : MemVectorL2 (cubeSet Q) u) (s : ℝ) (N : ℕ) : (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ≤ √2 * (cubeBesovNegativeVectorPartialSeminormTwo Q s N u + cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x)

theorem HCPolySupport.MeanZeroNeumannCorrectorData.cubeBesovNegativeVectorPartialSeminormTwo_corrector_le_sqrtTwo_mul_add_of_bounds {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) {u : Vec d → Vec d} (w : AHarmonicFunction a (cubeSet Q)) (huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) (hu : MemVectorL2 (cubeSet Q) u) (s : ℝ) {Bu Bw : ℝ} (huB : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminormTwo Q s N u ≤ Bu) (hwB : ∀ (N : ℕ), (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x) ≤ Bw) (N : ℕ) : (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ≤ √2 * (Bu + Bw)

theorem HCPolySupport.MeanZeroNeumannCorrectorData.cubeBesovNegativeVectorPartialSeminormTwo_corrector_le_sqrtTwo_mul_add_of_bddAbove {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) {u : Vec d → Vec d} (w : AHarmonicFunction a (cubeSet Q)) (huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) (hu : MemVectorL2 (cubeSet Q) u) (s : ℝ) (huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u)) (hwBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x)) (N : ℕ) : (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ≤ √2 * (cubeBesovNegativeVectorSeminormTwo Q s u + cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => w.toH1.grad x)

theorem HCPolySupport.MeanZeroNeumannCorrectorData.coefficientEnergy_average_le_note_terms_of_partialBounds_centered_two_two {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) (s : ℝ) {Bω Bg : ℝ} (hs : 0 < s) (hg_mem : MemVectorL2 (cubeSet Q) g) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hgradω : MeasureTheory.MemLp (fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) 2 (normalizedCubeMeasure Q)) (hBg : 0 ≤ Bg) (hneg : ∀ (N : ℕ), (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ≤ Bω) (hpos : ∀ (N : ℕ), (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g) ≤ Bg) : cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ≤ ∑ i : Fin d, (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bω) + cubeBesovScaleWeight s Q * ‖cubeAverage Q fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x i‖) * (cubeBesovScaleWeight s Q * Bg)

Corrector energy bound from the centered Neumann energy identity and the componentwise q = 2 Besov pairing estimate.

This is the Lean counterpart of manuscript Section 3.2.3, Step 2, before the remaining average term for grad omega is absorbed into a local negative Besov bound.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.coefficientEnergy_average_le_sharp_note_terms_of_partialBounds_centered_two_two {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) (s : ℝ) {Bω Bg : ℝ} (hs : 0 < s) (hg_mem : MemVectorL2 (cubeSet Q) g) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hgradω : MeasureTheory.MemLp (fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) 2 (normalizedCubeMeasure Q)) (hBg : 0 ≤ Bg) (hneg : ∀ (N : ℕ), (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ≤ Bω) (hpos : ∀ (N : ℕ), (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g) ≤ Bg) : cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ≤ ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bω) * (cubeBesovScaleWeight s Q * Bg))

Sharp corrector energy bound from the centered Neumann energy identity and the componentwise q = 2 Besov pairing estimate.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.coefficientEnergy_average_le_collapsed_note_term_centered_two_two {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) (s : ℝ) {Bω Bg : ℝ} (hs : 0 < s) (hg_mem : MemVectorL2 (cubeSet Q) g) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hgradω : MeasureTheory.MemLp (fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) 2 (normalizedCubeMeasure Q)) (hBg : 0 ≤ Bg) (hneg : ∀ (N : ℕ), (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ≤ Bω) (hpos : ∀ (N : ℕ), (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g) ≤ Bg) : cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ≤ ↑d * (3 ^ (↑d + s) * Bω * Bg)

Collapsed sharp corrector energy bound with the opposite scale weights canceled.