Coarse-graining support: Support.Deterministic.ConstantCoefficientDirichletBesov.OverlapPoincare

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

theorem HCPolySupport.overlapCubeLpNorm_two_overlapCubeFluctuationVec_toField_le_scale_mul_sum_grad {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (G : CubeVectorH1Function Q) (hS : S ∈ overlapCentersAtDepth Q j) : overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S G.toField) ≤ overlapCubeScaleFactor S * (originCubeMeanZeroH1CoerciveEstimate d 0).constantValue * ∑ i : Fin d, overlapCubeLpNorm S 2 (G.restrictCoordToOpenOverlap hS i).grad

theorem HCPolySupport.overlapCubeLpNorm_two_overlapCubeFluctuationVec_toField_le_scale_mul_sum_parent_grad {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (G : CubeVectorH1Function Q) (hS : S ∈ overlapCentersAtDepth Q j) : overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S G.toField) ≤ overlapCubeScaleFactor S * (originCubeMeanZeroH1CoerciveEstimate d 0).constantValue * ∑ i : Fin d, overlapCubeLpNorm S 2 (G.coord i).grad

theorem HCPolySupport.overlapCentersAverage_finset_sum {d : ℕ} {ι : Type u_1} (Q : TriadicCube d) (j : ℕ) (s : Finset ι) (F : ι → TriadicCube d → ℝ) : (overlapCentersAverage Q j fun (S : TriadicCube d) => ∑ i ∈ s, F i S) = ∑ i ∈ s, overlapCentersAverage Q j fun (S : TriadicCube d) => F i S

theorem HCPolySupport.overlapCentersAverage_overlapCubeLpNorm_grad_sq_le {d : ℕ} (Q : TriadicCube d) (j : ℕ) (G : CubeVectorH1Function Q) (i : Fin d) : (overlapCentersAverage Q j fun (S : TriadicCube d) => overlapCubeLpNorm S 2 (G.coord i).grad ^ 2) ≤ 3 ^ d * cubeLpNorm Q 2 (G.coord i).grad ^ 2

theorem HCPolySupport.cubeLpNorm_two_grad_le_volume_inv_rpow_half_mul_gradientCoordL2NormSum {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) : cubeLpNorm Q 2 u.grad ≤ (cubeVolume Q)⁻¹ ^ (1 / 2) * u.gradientCoordL2NormSum

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage_toField_le_raw {d : ℕ} (Q : TriadicCube d) (j : ℕ) (G : CubeVectorH1Function Q) : cubeBesovOverlappingPositiveVectorDepthAverage Q G.toField j ≤ (cubeScaleFactor Q / 3 ^ j * (originCubeMeanZeroH1CoerciveEstimate d 0).constantValue) ^ 2 * (↑(Fintype.card (Fin d)) * (3 ^ d * ((cubeVolume Q)⁻¹ ^ (1 / 2) * G.gradientCoordL2NormSum) ^ 2))

noncomputable def HCPolySupport.cubeVectorH1OverlapPoincareConstant (d : ℕ) : ℝ

Explicit constant for the averaged overlap-cube Poincare estimate.

Equations

• HCPolySupport.cubeVectorH1OverlapPoincareConstant d = √(↑(Fintype.card (Fin d)) * 3 ^ d) * (HCPolySupport.originCubeMeanZeroH1CoerciveEstimate d 0).constantValue

theorem HCPolySupport.cubeVectorH1OverlapPoincareConstant_nonneg (d : ℕ) : 0 ≤ cubeVectorH1OverlapPoincareConstant d

def HCPolySupport.CubeVectorH1OverlapPoincareEstimate (d : ℕ) (C : ℝ) : Prop

Averaged overlap-cube Poincare estimate for coordinatewise H¹ vector competitors.

This is the scale-correct analytic input for the competitor branch of the pure K/overlapping comparison. The overlapping oscillations are normalized L² quantities, while the H¹ competitor carries a raw parent-cube gradient norm, so the parent-normalized size relativeGradientCoordL2NormSum appears.

Equations

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

theorem HCPolySupport.cubeVectorH1OverlapPoincareEstimate (d : ℕ) : CubeVectorH1OverlapPoincareEstimate d (cubeVectorH1OverlapPoincareConstant d)

theorem HCPolySupport.exists_cubeVectorH1OverlapPoincareEstimate (d : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ CubeVectorH1OverlapPoincareEstimate d C

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage_toField_le_of_overlapPoincare {d : ℕ} {C : ℝ} (hC : 0 ≤ C) (hPoincare : CubeVectorH1OverlapPoincareEstimate d C) (Q : TriadicCube d) (j : ℕ) (G : CubeVectorH1Function Q) : cubeBesovOverlappingPositiveVectorDepthAverage Q G.toField j ≤ (C * Real.rpow 3 (-↑j) * G.relativeGradientCoordL2NormSum) ^ 2