Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.PrintOrderToleranceSelectedRoundedSpine

High-contrast homogenization: Provider.Regularity.PrintOrderToleranceSelectedRoundedSpine #

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

One rounded generation selected from the absorption tolerance #

The generation is selected after the identity estimate and before any coefficient sample or target amplitude. All later applications therefore use the same deterministic geometry.

source
theorem HCPolySupport.HighContrast.sharp_order_bounds_of_selected_defect {d : ℕ} {A : Mat d} (hA : Matrix.PosDef A) (hdefect : ‖A - 1‖ ≤ 1 / 100) :
(99 / 100) • 1 ≤ A ∧ A ≤ (101 / 100) • 1
source
structure HCPolySupport.HighContrast.PrintOrderToleranceSelectedRoundedSpine (d : ℕ) [NeZero d] (Cid : ℝ) :
Type

Uniform data of the generation chosen at the private spine tolerance.

Instances For
    source
    theorem HCPolySupport.HighContrast.PrintOrderToleranceSelectedRoundedSpine.absorptionProperties {d : ℕ} [NeZero d] {Cid : ℝ} (spine : PrintOrderToleranceSelectedRoundedSpine d Cid) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) :
    Matrix.PosDef (roundedReferenceMatrixAtGeneration spine.generation abar hS) ∧ IsEllipticMatrix (1 - printOrderAbsorptionTolerance d Cid) (1 + printOrderAbsorptionTolerance d Cid) (roundedReferenceMatrixAtGeneration spine.generation abar hS) ∧ ‖roundedReferenceMatrixAtGeneration spine.generation abar hS - 1‖ ≤ printOrderAbsorptionTolerance d Cid

    The selected matrices satisfy the exact absorption window.

    source
    def HCPolySupport.HighContrast.PrintOrderToleranceSelectedRoundedSpine.geometry {d : ℕ} [NeZero d] {Cid : ℝ} (spine : PrintOrderToleranceSelectedRoundedSpine d Cid) :
    RoundedGenerationAnalyticGeometry d

    The selected generation as the common deterministic geometry.

    Equations
    • spine.geometry = { generation := spine.generation, admissible := ⋯, reference_posDef := ⋯, reference_elliptic := ⋯, reference_lower := ⋯, reference_upper := ⋯ }
    Instances For
      source
      theorem HCPolySupport.HighContrast.nonempty_printOrderToleranceSelectedRoundedSpine (d : ℕ) [NeZero d] (Cid : ℝ) :
      Nonempty (PrintOrderToleranceSelectedRoundedSpine d Cid)

      The tolerance constructor supplies one uniform selected generation.

      source
      theorem HCPolySupport.HighContrast.PrintOrderQuantitativeNormalizedReferenceCertificate.exists_applicationAtSelectedSpine {d : ℕ} [NeZero d] {g : ℝ} {a : CoeffSpace d} {abar : Mat d} {sourceAmplitude target kappa Cid : ℝ} {X : CoeffSpace d → ℝ} (h : PrintOrderQuantitativeNormalizedReferenceCertificate abar g sourceAmplitude kappa (X a) a) (spine : PrintOrderToleranceSelectedRoundedSpine d Cid) (hg : g ∈ Set.Ico 0 1) (hTarget : 0 < target) (hidentity : PrintOrderIdentityCubeDualRegularityWithConstant d g Cid) :
      ∃ (application : PrintOrderParametricRoundedCoefficientApplication d g a abar sourceAmplitude target kappa Cid X), application.generation = spine.generation

      A certificate is applied at a previously selected rounded generation, with the generation equality retained for downstream consumers.

      source
      theorem HCPolySupport.HighContrast.PrintOrderQuantitativeNormalizedReferenceCertificate.exists_joinAtSelectedSpine {d : ℕ} [NeZero d] {g : ℝ} {a : CoeffSpace d} {abar : Mat d} {sourceAmplitude target kappa Cid : ℝ} {X : CoeffSpace d → ℝ} (h : PrintOrderQuantitativeNormalizedReferenceCertificate abar g sourceAmplitude kappa (X a) a) (spine : PrintOrderToleranceSelectedRoundedSpine d Cid) (hg : g ∈ Set.Ico 0 1) (hTarget : 0 < target) (hidentity : PrintOrderIdentityCubeDualRegularityWithConstant d g Cid) :
      ∃ (join : PrintOrderParametricRoundedResponseJoin d g a abar sourceAmplitude target kappa Cid X), join.application.generation = spine.generation

      Generation-preserving selected join for terminal assembly.