High-contrast homogenization:

Provider.Regularity.RoundedUnitCubeDirichletContinuousKIterationEnergyLimit

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

Positive-order energy at the rounded affine iteration limit

Right-associated finite tails of the geometric increments have a uniform continuous-K energy bound: the factor two from each addition is absorbed by the much faster geometric contraction. The continuous K-functional is Lipschitz with respect to the base Hilbert L² distance. Pointwise convergence of its weighted integrand and Fatou's lemma therefore pass the uniform positive-order bound to the identified zero-trace weak limit.

noncomputable def HCPolySupport.HighContrast.roundedUnitCubeDirichletContinuousKIterationIncrementTail {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : UnitCubeEuclideanL2Field d) (k : ℕ) : ℕ → UnitCubeEuclideanL2Field d

A right-associated nonempty tail of consecutive rounded iteration increments. Index n represents the n + 1 increments beginning at k.

Equations

• One or more equations did not get rendered due to their size.
• HCPolySupport.HighContrast.roundedUnitCubeDirichletContinuousKIterationIncrementTail abar hS h k 0 = HCPolySupport.HighContrast.roundedUnitCubeDirichletContinuousKIterationIncrement abar hS h k

theorem HCPolySupport.HighContrast.roundedUnitCubeDirichletContinuousKIterationIncrementTail_apply {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : UnitCubeEuclideanL2Field d) (k n : ℕ) (x : Vec d) : (roundedUnitCubeDirichletContinuousKIterationIncrementTail abar hS h k n).toField x = (roundedUnitCubeDirichletContinuousKIteration abar hS h (k + n + 1)).grad x - (roundedUnitCubeDirichletContinuousKIteration abar hS h k).grad x

A right-associated increment tail telescopes to the literal difference of its endpoint iteration gradients.

theorem HCPolySupport.HighContrast.roundedUnitCubeDirichletContinuousKIterationIncrementTail_zero_eq_gradient {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : UnitCubeEuclideanL2Field d) (n : ℕ) : roundedUnitCubeDirichletContinuousKIterationIncrementTail abar hS h 0 n = unitCubeGradientEuclideanL2Field (roundedUnitCubeDirichletContinuousKIteration abar hS h (n + 1))

Starting the right-associated tail at zero gives exactly the packaged gradient of the corresponding positive iterate.

theorem HCPolySupport.HighContrast.roundedUnitCubeDirichletContinuousKIterationIncrementTail_energy_le {d : ℕ} [NeZero d] (s : ↑FractionalOrder) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : UnitCubeEuclideanL2Field d) (q E0 : ENNReal) (hq : q ≤ ENNReal.ofReal (1 / 4)) (hincrements : ∀ (j : ℕ), unitCubeNormalizedContinuousKEnergy s (roundedUnitCubeDirichletContinuousKIterationIncrement abar hS h j) ≤ q ^ j * E0) (k n : ℕ) : unitCubeNormalizedContinuousKEnergy s (roundedUnitCubeDirichletContinuousKIterationIncrementTail abar hS h k n) ≤ 4 * (q ^ k * E0)

Right association turns the factor-two addition estimate into a uniform bound because the next tail starts one geometric power later.

theorem HCPolySupport.HighContrast.continuousKFunctional_le_norm_unitCubeEuclideanL2FieldHilbertL2 {d : ℕ} (t : ↑ContinuousKScale) (F : UnitCubeEuclideanL2Field d) : continuousKFunctional t F ≤ ‖unitCubeEuclideanL2FieldHilbertL2 F‖

The continuous K-functional is bounded by the base Hilbert L² norm, using the zero competitor.

theorem HCPolySupport.HighContrast.abs_continuousKFunctional_sub_le_dist_hilbertL2 {d : ℕ} (t : ↑ContinuousKScale) (F G : UnitCubeEuclideanL2Field d) : |continuousKFunctional t F - continuousKFunctional t G| ≤ dist (unitCubeEuclideanL2FieldHilbertL2 F) (unitCubeEuclideanL2FieldHilbertL2 G)

The continuous K-functional is one-Lipschitz with respect to the base Hilbert L² distance.

theorem HCPolySupport.HighContrast.tendsto_continuousKFunctional_of_tendsto_hilbertL2 {d : ℕ} (t : ↑ContinuousKScale) (F : ℕ → UnitCubeEuclideanL2Field d) (G : UnitCubeEuclideanL2Field d) (hFG : Filter.Tendsto (fun (n : ℕ) => unitCubeEuclideanL2FieldHilbertL2 (F n)) Filter.atTop (nhds (unitCubeEuclideanL2FieldHilbertL2 G))) : Filter.Tendsto (fun (n : ℕ) => continuousKFunctional t (F n)) Filter.atTop (nhds (continuousKFunctional t G))

Base Hilbert L² convergence implies convergence of every fixed-scale continuous K-functional value.

theorem HCPolySupport.HighContrast.tendsto_continuousKSeminormIntegrand_of_tendsto_hilbertL2 {d : ℕ} (sigma : ℝ) (F : ℕ → UnitCubeEuclideanL2Field d) (G : UnitCubeEuclideanL2Field d) (hFG : Filter.Tendsto (fun (n : ℕ) => unitCubeEuclideanL2FieldHilbertL2 (F n)) Filter.atTop (nhds (unitCubeEuclideanL2FieldHilbertL2 G))) (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => continuousKSeminormIntegrand sigma (F n) t) Filter.atTop (nhds (continuousKSeminormIntegrand sigma G t))

Base Hilbert L² convergence gives pointwise convergence of the weighted continuous-K seminorm integrands.

theorem HCPolySupport.HighContrast.unitCubeNormalizedContinuousKEnergy_limit_le_two_mul {d : ℕ} (s : ↑FractionalOrder) (F : ℕ → UnitCubeEuclideanL2Field d) (G : UnitCubeEuclideanL2Field d) (M : ENNReal) (hFG : Filter.Tendsto (fun (n : ℕ) => unitCubeEuclideanL2FieldHilbertL2 (F n)) Filter.atTop (nhds (unitCubeEuclideanL2FieldHilbertL2 G))) (hbound : ∀ (n : ℕ), unitCubeNormalizedContinuousKEnergy s (F n) ≤ M) : unitCubeNormalizedContinuousKEnergy s G ≤ 2 * M

A uniform continuous-K energy bound is closed under base Hilbert L² convergence. Separating the endpoint and continuum terms costs only the displayed factor two.

theorem HCPolySupport.HighContrast.exists_roundedUnitCubeDirichletContinuousKIterationEnergyLimit (d : ℕ) [NeZero d] : ∃ (A : ℝ), 1 ≤ A ∧ ∃ (s : ↑FractionalOrder), ↑s < 1 / 12 ∧ ENNReal.ofReal A ^ (2 * ↑s) < ENNReal.ofReal (101 / 100) ∧ ENNReal.ofReal A ^ (2 * ↑s) * ENNReal.ofReal ((1 / 100) ^ 2) < ENNReal.ofReal (101 / 1000000) ∧ ENNReal.ofReal A ^ (2 * ↑s) * ENNReal.ofReal ((1 / 100) ^ 2) < 1 ∧ ∃ (B : ℝ), 1 ≤ B ∧ ∀ (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : UnitCubeEuclideanL2Field d), unitCubeNormalizedContinuousKEnergy s h < ⊤ → ∃ (u : H10Function (openCubeSet (originCube d 0))), Filter.Tendsto (roundedUnitCubeDirichletContinuousKIterationGradientHilbertL2 abar hS h) Filter.atTop (nhds u.gradToHilbertVectorL2) ∧ (IsZeroTraceDirichletRhsWeakSolution (constantCoeffField (roundedReferenceMatrix abar hS)) (openCubeSet (originCube d 0)) u fun (x : Vec d) => -h.toField x) ∧ unitCubeNormalizedContinuousKEnergy s (unitCubeGradientEuclideanL2Field u) ≤ 8 * (ENNReal.ofReal B ^ (2 * ↑s) * unitCubeNormalizedContinuousKEnergy s h) ∧ unitCubeNormalizedContinuousKEnergy s (unitCubeGradientEuclideanL2Field u) < ⊤

The rounded-reference weak limit inherits a finite selected-order continuous-K energy, with all membership and finiteness asserted as conclusions.