Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.Boundary.NoteRhs.StandardSplit

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

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross : ℝ) : ℝ

The explicit split boundary constant σ(max(A / K, 0) + 1)^(1 / p), with A, K, and p given by the boundary height and ellipticity quantities; zero when LambdaSq vanishes.

Equations

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

theorem HCPolySupport.coarseCaccioppoliBoundaryStandardExplicitHeightCoeffSplit_eq_zero_of_LambdaSq_eq_zero {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross : ℝ) (hΛ : LambdaSq Q s (MultiscaleExponent.finite 1) a = 0) : coarseCaccioppoliBoundaryStandardExplicitHeightCoeffSplit Q a s t Calpha Ccross = 0

theorem HCPolySupport.coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit_nonneg_of_thetaRatio_pos {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross : ℝ) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hTheta : 0 < ThetaRatio Q s t a) : 0 ≤ coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit Q a s t Calpha Ccross

theorem HCPolySupport.coarseCaccioppoliBoundaryStandardExplicitHeightCoeffSplit_div_kernel_le_explicit {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross : ℝ) (hCalpha : 0 < Calpha) (hCcross : 0 ≤ Ccross) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hTheta : 1 ≤ ThetaRatio Q s t a) : have σ := coarseCaccioppoliSigma s t; have q := coarseCaccioppoliPower s t; have K := s.rpow (-2 * s / σ) * (ThetaRatio Q s t a).rpow (s / σ) * LambdaSq Q s (MultiscaleExponent.finite 1) a; have R := coarseCaccioppoliStandardRadiusIterationConst (coarseCaccioppoliBeta s t); have B₁ := 6561 * 6561 * Ccross ^ 2; have B₂ := 9 * Real.rpow 4 q * Real.rpow 81 q * Ccross * Ccross * Calpha.rpow q * (1 - s).rpow (-q); coarseCaccioppoliBoundaryStandardExplicitHeightCoeffSplit Q a s t Calpha Ccross / K ≤ R * (B₁ + B₂)

theorem HCPolySupport.coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit_le_of_heightCoeff_div_kernel_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross B Ctarget : ℝ) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hB : 0 ≤ B) (hdiv : have σ := coarseCaccioppoliSigma s t; have K := s.rpow (-2 * s / σ) * (ThetaRatio Q s t a).rpow (s / σ) * LambdaSq Q s (MultiscaleExponent.finite 1) a; have A := coarseCaccioppoliBoundaryStandardExplicitHeightCoeffSplit Q a s t Calpha Ccross; A / K ≤ B) (hCtarget : have σ := coarseCaccioppoliSigma s t; have p := 2 + 4 * s / σ; σ * (B + 1).rpow p⁻¹ ≤ Ctarget) : coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit Q a s t Calpha Ccross ≤ Ctarget

Scalar extraction lemma for the exposed explicit note constant.

Once the height coefficient divided by the note kernel is bounded by a scalar B, the explicit note constant is bounded by the displayed note-scale root. This is the coefficient-cancellation step needed before choosing a uniform dimension-only public constant.

theorem HCPolySupport.coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit_le_explicitBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross : ℝ) (hCalpha : 0 < Calpha) (hCcross : 0 ≤ Ccross) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hTheta : 1 ≤ ThetaRatio Q s t a) : have σ := coarseCaccioppoliSigma s t; have p := 2 + 4 * s / σ; have q := coarseCaccioppoliPower s t; have R := coarseCaccioppoliStandardRadiusIterationConst (coarseCaccioppoliBeta s t); have B₁ := 6561 * 6561 * Ccross ^ 2; have B₂ := 9 * Real.rpow 4 q * Real.rpow 81 q * Ccross * Ccross * Calpha.rpow q * (1 - s).rpow (-q); have B := R * (B₁ + B₂); coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit Q a s t Calpha Ccross ≤ σ * (B + 1).rpow p⁻¹

theorem HCPolySupport.boundaryCaccioppoliHeightCoefficientSplit_le_noteConstantSplit {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross : ℝ) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hTheta : 0 < ThetaRatio Q s t a) : coarseCaccioppoliBoundaryStandardExplicitHeightCoeffSplit Q a s t Calpha Ccross ≤ coarseCaccioppoliBoundaryNoteCoeff Q a s t (coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit Q a s t Calpha Ccross)

theorem HCPolySupport.boundaryCaccioppoliHeightBound_le_rhsConstantSplit {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hTheta : 0 < ThetaRatio Q s t a) : coarseCaccioppoliBoundaryStandardExplicitHeightBoundSplit Q a s t Calpha Ccross uL2Sq ≤ coarseCaccioppoliBoundaryNoteRhs Q a s t (coarseCaccioppoliBoundaryStandardExplicitNoteConstantSplit Q a s t Calpha Ccross) uL2Sq

Standard split coefficient-level note-RHS comparison after the non-degenerate multiscale factor ThetaRatio has been identified as positive.