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

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

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryRecursionCoeff {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) : ℝ

Boundary recursion prefactor with the public uL2Sq factor removed.

Equations

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

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

Split recursion prefactor with the public uL2Sq factor removed.

Equations

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

theorem HCPolySupport.coarseCaccioppoliBoundaryRecursionCoeffSplit_self {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) : coarseCaccioppoliBoundaryRecursionCoeffSplit Q a s t C C = coarseCaccioppoliBoundaryRecursionCoeff Q a s t C

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightRecursionCoeff {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) : ℝ

Explicit-height recursion prefactor with the public uL2Sq factor removed.

Equations

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

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

Split explicit-height recursion prefactor with the public uL2Sq factor removed. The left branch depends only on Ccross; the logarithmic branch depends on Calpha through the height and on Ccross through the cross term.

Equations

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

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightRecursionCoeffSplit_self {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) : coarseCaccioppoliBoundaryExplicitHeightRecursionCoeffSplit Q a s t C C = coarseCaccioppoliBoundaryExplicitHeightRecursionCoeff Q a s t C

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightCoeff {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) : ℝ

Explicit-height radius-iteration prefactor with uL2Sq removed.

Equations

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

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

Split explicit-height prefactor using the standard beta-dependent radius iteration. This is the coefficient surface for the note-facing route, carrying the standard (C beta)^beta iteration loss.

Equations

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

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

Standard-radius split explicit-height bound, before conversion to the public note RHS.

Equations

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

noncomputable def HCPolySupport.coarseCaccioppoliBoundaryNoteCoeff {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) : ℝ

Literal note RHS prefactor with the public uL2Sq factor removed.

Equations

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

theorem HCPolySupport.coarseCaccioppoliBoundaryRecursionRhs_eq_coeff_mul_uL2Sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) : coarseCaccioppoliBoundaryRecursionRhs Q a s t C uL2Sq = coarseCaccioppoliBoundaryRecursionCoeff Q a s t C * uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryRecursionRhsSplit_eq_coeff_mul_uL2Sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) : coarseCaccioppoliBoundaryRecursionRhsSplit Q a s t Calpha Ccross uL2Sq = coarseCaccioppoliBoundaryRecursionCoeffSplit Q a s t Calpha Ccross * uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightRecursionRhs_eq_coeff_mul_uL2Sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) : coarseCaccioppoliBoundaryExplicitHeightRecursionRhs Q a s t C uL2Sq = coarseCaccioppoliBoundaryExplicitHeightRecursionCoeff Q a s t C * uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightRecursionRhsSplit_eq_coeff_mul_uL2Sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) : coarseCaccioppoliBoundaryExplicitHeightRecursionRhsSplit Q a s t Calpha Ccross uL2Sq = coarseCaccioppoliBoundaryExplicitHeightRecursionCoeffSplit Q a s t Calpha Ccross * uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightBound_eq_coeff_mul_uL2Sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) : coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq = coarseCaccioppoliBoundaryExplicitHeightCoeff Q a s t C * uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryStandardExplicitHeightBoundSplit_eq_coeff_mul_uL2Sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) : coarseCaccioppoliBoundaryStandardExplicitHeightBoundSplit Q a s t Calpha Ccross uL2Sq = coarseCaccioppoliBoundaryStandardExplicitHeightCoeffSplit Q a s t Calpha Ccross * uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryNoteRhs_eq_coeff_mul_uL2Sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) : coarseCaccioppoliBoundaryNoteRhs Q a s t C uL2Sq = coarseCaccioppoliBoundaryNoteCoeff Q a s t C * uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryRecursionRhs_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) : 0 ≤ coarseCaccioppoliBoundaryRecursionRhs Q a s t C uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryRecursionRhsSplit_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (hCalpha : 0 ≤ Calpha) (hCcross : 0 ≤ Ccross) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) : 0 ≤ coarseCaccioppoliBoundaryRecursionRhsSplit Q a s t Calpha Ccross uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightRecursionRhs_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) : 0 ≤ coarseCaccioppoliBoundaryExplicitHeightRecursionRhs Q a s t C uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightRecursionRhsSplit_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Calpha Ccross uL2Sq : ℝ) (hCalpha : 0 ≤ Calpha) (hCcross : 0 ≤ Ccross) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) : 0 ≤ coarseCaccioppoliBoundaryExplicitHeightRecursionRhsSplit Q a s t Calpha Ccross uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryBound_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) : 0 ≤ coarseCaccioppoliBoundaryBound Q a s t C uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightBound_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) : 0 ≤ coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryRecursionCoeff_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : 0 ≤ coarseCaccioppoliBoundaryRecursionCoeff Q a s t C

theorem HCPolySupport.coarseCaccioppoliBoundaryRecursionCoeffSplit_nonneg {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) : 0 ≤ coarseCaccioppoliBoundaryRecursionCoeffSplit Q a s t Calpha Ccross

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightRecursionCoeff_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : 0 ≤ coarseCaccioppoliBoundaryExplicitHeightRecursionCoeff Q a s t C

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightRecursionCoeffSplit_nonneg {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) : 0 ≤ coarseCaccioppoliBoundaryExplicitHeightRecursionCoeffSplit Q a s t Calpha Ccross

theorem HCPolySupport.coarseCaccioppoliBoundaryExplicitHeightCoeff_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : 0 ≤ coarseCaccioppoliBoundaryExplicitHeightCoeff Q a s t C

theorem HCPolySupport.coarseCaccioppoliBoundaryNoteRhs_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) : 0 ≤ coarseCaccioppoliBoundaryNoteRhs Q a s t C uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryNoteCoeff_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : 0 ≤ coarseCaccioppoliBoundaryNoteCoeff Q a s t C

theorem HCPolySupport.coarseCaccioppoliBoundaryNoteCoeff_mono_C {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C₁ C₂ : ℝ) (hC₁ : 0 ≤ C₁) (hC₁C₂ : C₁ ≤ C₂) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : coarseCaccioppoliBoundaryNoteCoeff Q a s t C₁ ≤ coarseCaccioppoliBoundaryNoteCoeff Q a s t C₂

theorem HCPolySupport.coarseCaccioppoliBoundaryNoteRhs_mono_C {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C₁ C₂ uL2Sq : ℝ) (hC₁ : 0 ≤ C₁) (hC₁C₂ : C₁ ≤ C₂) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) : coarseCaccioppoliBoundaryNoteRhs Q a s t C₁ uL2Sq ≤ coarseCaccioppoliBoundaryNoteRhs Q a s t C₂ uL2Sq

theorem HCPolySupport.coarseCaccioppoliBoundaryNoteCoeff_mul_const_le_of_mul_constant_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t M C₁ C₂ : ℝ) (hM : 1 ≤ M) (hC₁ : 0 ≤ C₁) (hMC₁C₂ : M * C₁ ≤ C₂) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : M * coarseCaccioppoliBoundaryNoteCoeff Q a s t C₁ ≤ coarseCaccioppoliBoundaryNoteCoeff Q a s t C₂

theorem HCPolySupport.coarseCaccioppoliBoundaryNoteRhs_mul_const_le_of_mul_constant_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t M C₁ C₂ uL2Sq : ℝ) (hM : 1 ≤ M) (hC₁ : 0 ≤ C₁) (hMC₁C₂ : M * C₁ ≤ C₂) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) : M * coarseCaccioppoliBoundaryNoteRhs Q a s t C₁ uL2Sq ≤ coarseCaccioppoliBoundaryNoteRhs Q a s t C₂ uL2Sq