High-contrast homogenization: Provider.Quenched.SmallContrastSharpConstant

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The isotropy recursion constant without geometric slack

The drop branch of the isotropic fusion recursion constant is

dropCoefficient d Cpre eta * (((3 ^ (-recursionAlpha g)) ^ H)⁻¹ * (1 - 3 ^ (-recursionAlpha g))⁻¹)
  + 3 * weakCoefficient d Cpre * weakDropConstant …

The factor (1 - r)⁻¹ produces the lower bound A ≳ 1 / alpha. The definition fusionRecursionConstantIsotropySharp removes this factor from the same maximum, as permitted by SmallContrastSharpDrop.hrec_final_sharp.

The comparison fusionRecursionConstantIsotropySharp ≤ fusionRecursionConstantIso certifies that the replacement is a genuine improvement and never a weakening: (1 - r)⁻¹ ≥ 1 for 0 < r < 1, so every use site that needed the old constant as an upper bound is still served.

noncomputable def HCPolySupport.HighContrast.Quenched.fusionRecursionConstantIsotropySharp (d : ℕ) (Cpre eta : ℝ) (H : ℕ) (M L g cRow kap cD delta cVsum cVm : ℝ) : ℝ

The sharp isotropy recursion constant. The isotropic fusion recursion constant with the geometric factor (1 - 3 ^ (-recursionAlpha g))⁻¹ removed from the drop branch. Licensed by hrec_final_sharp_at_jb_src, whose hA1 slot is a * (r ^ H)⁻¹ + 3 * cw * cdrop ≤ A.

Equations

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

theorem HCPolySupport.HighContrast.Quenched.one_le_fusionRecursionConstantIsotropySharp (d : ℕ) (Cpre eta : ℝ) (H : ℕ) (M L g cRow kap cD delta cVsum cVm : ℝ) : 1 ≤ fusionRecursionConstantIsotropySharp d Cpre eta H M L g cRow kap cD delta cVsum cVm

theorem HCPolySupport.HighContrast.Quenched.ratio_mem_Ioo {g : ℝ} (hg1 : g < 1) : 0 < 3 ^ (-recursionAlpha g) ∧ 3 ^ (-recursionAlpha g) < 1

The one-step ratio lies in (0,1) whenever g < 1.