High-contrast homogenization: Setup.AnalyticCarriers

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

Analytic carriers for the homogenization theorem

The volume-normalized and coefficient-weighted spaces of s.introduction, the weak equation, the Liouville class, and the domain data carried by the Dirichlet estimate of t.random.homogenization.

This module carries definitions only. Every norm and energy is valued in ℝ≥0∞: the integrands are nonnegative, so the Lebesgue integral is defined for every argument and is infinite exactly where the quantity the reference text writes is infinite, whereas a totalized Bochner integral would return zero there and let an estimate be satisfied by the failure of the membership it presupposes. The two dual norms and the weak equation carry the absolute convergence of their pairings for the same reason: it is the well-formedness of a printed distributional display, not an additional claim. The membership classes carry the measurability of their pairs, which their printed counterparts — completions of smooth functions in a norm — presuppose.

Elementary geometry and pointwise operations

def HCPolySupport.HighContrast.euclideanBallAt {d : ℕ} (c : Vec d) (r : ℝ) : Set (Vec d)

The open Euclidean ball of radius r centered at c. The ambient norm of Vec d is the supremum norm, so the Euclidean radius is written through vecNormSq.

Equations

• HCPolySupport.HighContrast.euclideanBallAt c r = {x : HCPolySupport.Vec d | HCPolySupport.vecNormSq (x - c) < r ^ 2}

def HCPolySupport.HighContrast.euclideanBall (d : ℕ) (r : ℝ) : Set (Vec d)

The open Euclidean ball B_r centered at the origin.

Equations

• HCPolySupport.HighContrast.euclideanBall d r = HCPolySupport.HighContrast.euclideanBallAt 0 r

noncomputable def HCPolySupport.HighContrast.smoothGrad {d : ℕ} (f : Vec d → ℝ) (x : Vec d) : Vec d

The coordinate gradient of a smooth scalar function, through fderiv.

Equations

• HCPolySupport.HighContrast.smoothGrad f x i = (fderiv ℝ f x) (HCPolySupport.basisVec i)

noncomputable def HCPolySupport.HighContrast.scaledCoeff {d : ℕ} (ε : ℝ) (a : CoeffSpace d) : CoeffField d

The rescaled sample coefficient a^ε(x) = a(x/ε).

Equations

• HCPolySupport.HighContrast.scaledCoeff ε a x = ↑↑a (ε⁻¹ • x)

structure HCPolySupport.HighContrast.IsLocalVecTest {d : ℕ} (U : Set (Vec d)) (ψ : Vec d → Vec d) : Prop

A vector-valued test function on U: smooth, compactly supported inside U.

• contDiff : ContDiff ℝ (↑⊤) ψ
• hasCompactSupport : HasCompactSupport ψ
• tsupport_subset : tsupport ψ ⊆ U

Normalized norms (the volume-normalized function spaces)

All norms and energies below are valued in ℝ≥0∞. Their integrands are nonnegative, so the Lebesgue integral is defined for every argument and takes the value ∞ exactly when the quantity the reference text writes is infinite; a Bochner integral would instead return 0 there, which would make each estimate satisfiable by the failure of the very membership it presupposes.

noncomputable def HCPolySupport.HighContrast.eVolumeAverage {d : ℕ} (V : Set (Vec d)) (f : Vec d → ENNReal) : ENNReal

The volume-normalized integral ⨍_V f of a nonnegative quantity.

Equations

• HCPolySupport.HighContrast.eVolumeAverage V f = (∫⁻ (x : HCPolySupport.Vec d) in V, f x) / MeasureTheory.volume V

noncomputable def HCPolySupport.HighContrast.normalizedL2Norm {d : ℕ} (V : Set (Vec d)) (v : Vec d → ℝ) : ENNReal

The normalized norm ‖v‖_{L_underlined²(V)} (the volume-normalized L^p norm at p = 2).

Equations

• HCPolySupport.HighContrast.normalizedL2Norm V v = (HCPolySupport.HighContrast.eVolumeAverage V fun (x : HCPolySupport.Vec d) => ENNReal.ofReal (v x ^ 2)) ^ (1 / 2)

noncomputable def HCPolySupport.HighContrast.weightedGradNorm {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) (F : Vec d → Vec d) : ENNReal

The value ‖s^{1/2} F‖_{L_underlined²(V)} for the symmetric part s of a coefficient field, written through the quadratic form (an exact identity, not a re-encoding).

Equations

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

noncomputable def HCPolySupport.HighContrast.fracSeminormSq {d : ℕ} (V : Set (Vec d)) (s : ℝ) (F : Vec d → Vec d) : ENNReal

The Gagliardo double-integral seminorm square of a vector field (e.physical.fractional.norm), with Euclidean distances.

Equations

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

noncomputable def HCPolySupport.HighContrast.hsNormSq {d : ℕ} (V : Set (Vec d)) (s : ℝ) (F : Vec d → Vec d) : ENNReal

The volume-normalized H^s(V) norm square of a vector field (e.physical.fractional.norm).

Equations

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

noncomputable def HCPolySupport.HighContrast.h1NormSq {d : ℕ} (V : Set (Vec d)) (ψ : Vec d → Vec d) : ENNReal

The volume-normalized H¹(V) norm square of a smooth vector test function (the s = 1 display of the volume-normalized function spaces), with componentwise gradients.

Equations

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

noncomputable def HCPolySupport.HighContrast.dualPairing {d : ℕ} (V : Set (Vec d)) (F ψ : Vec d → Vec d) : ENNReal

The normalized pairing ⨍_V F · ψ of a vector field against a test field, valued in ℝ≥0∞. A pairing that is not absolutely convergent is ∞: the reference text reads the pairing of a locally integrable field against a smooth compactly supported test, and a totalized Bochner integral would silently value a divergent pairing at 0, dropping that test from the supremum below.

Equations

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

noncomputable def HCPolySupport.HighContrast.negSobolevNorm {d : ℕ} (V : Set (Vec d)) (s : ℝ) (F : Vec d → Vec d) : ENNReal

The dual norm ‖F‖_{H^{-s}(V)} (e.physical.negative.norm).

Equations

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

noncomputable def HCPolySupport.HighContrast.negOneNorm {d : ℕ} (V : Set (Vec d)) (F : Vec d → Vec d) : ENNReal

The dual norm ‖F‖_{H_underlined^{-1}(V)} (the s = 1 display of the volume-normalized function spaces).

Equations

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

Coefficient-weighted Sobolev classes

(the coefficient Sobolev space)

noncomputable def HCPolySupport.HighContrast.sEnergyOn {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) (F : Vec d → Vec d) : ENNReal

The s-weighted Dirichlet energy ∫_V F · s F.

Equations

• HCPolySupport.HighContrast.sEnergyOn b V F = ∫⁻ (x : HCPolySupport.Vec d) in V, ENNReal.ofReal (HCPolySupport.vecDot (F x) (HCPolySupport.matVecMul (HCPolySupport.symmPart (b x)) (F x)))

noncomputable def HCPolySupport.HighContrast.h1sNormSqOn {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) (u : Vec d → ℝ) (Du : Vec d → Vec d) : ENNReal

The H¹_s(V) norm square ‖u‖_{L¹(V)}² + ∫_V ∇u · s ∇u.

Equations

• HCPolySupport.HighContrast.h1sNormSqOn b V u Du = (∫⁻ (x : HCPolySupport.Vec d) in V, ENNReal.ofReal |u x|) ^ 2 + HCPolySupport.HighContrast.sEnergyOn b V Du

noncomputable def HCPolySupport.HighContrast.skewFluxPairing {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) (F : Vec d → Vec d) (φ : Vec d → ℝ) : ENNReal

The pairing ∫_V ∇φ · k F of the skew flux against a test gradient, valued in ℝ≥0∞ and infinite on a pairing that is not absolutely convergent.

Equations

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

noncomputable def HCPolySupport.HighContrast.skewFluxDualNorm {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) (F : Vec d → Vec d) : ENNReal

The H^{-1}_s(V) norm of the skew flux divergence ∇·(k F), through smooth compactly supported tests of unit H¹_s norm.

Equations

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

def HCPolySupport.HighContrast.IsMeasurableGradientPair {d : ℕ} (μ : MeasureTheory.Measure (Vec d)) (u : Vec d → ℝ) (Du : Vec d → Vec d) : Prop

A function and a candidate gradient field for it, both measurable.

The reference text's coefficient-weighted spaces are completions of smooth functions in a norm, so each of their elements is an equivalence class of measurable functions carrying a measurable gradient field; the classes below record that. The condition is what makes the relation tying a function to its weak gradient an identity between convergent integrals: with it, and with the coefficient field elliptic almost everywhere, both pairings of that relation converge absolutely. Without it the relation compares two integrals that may each fail to converge, and a pair on which they both fail satisfies it for no reason; whether the wider class actually contains such a pair is a question about sets of inner measure zero, and is not settled here.

The condition is faithful in both directions. Where a membership class stands as a hypothesis, the narrower class makes the statement assert less; where it stands as a conclusion, as in the second inclusion of the Liouville clause, the narrower class makes it assert more, and that inclusion is the only place the measurability of the corrector family is asserted at all.

Equations

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

def HCPolySupport.HighContrast.MemH1a {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) (u : Vec d → ℝ) (Du : Vec d → Vec d) : Prop

Membership in H¹_a(V): a weak-gradient pair approximated by globally smooth functions in the H¹_a norm (H¹_s part and skew-flux dual part).

Equations

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

def HCPolySupport.HighContrast.MemH1a0 {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) (u : Vec d → ℝ) (Du : Vec d → Vec d) : Prop

Membership in H¹_{a,0}(V): as MemH1a, with the approximants compactly supported inside V.

Equations

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

def HCPolySupport.HighContrast.MemH1sLoc {d : ℕ} (b : CoeffField d) (v : Vec d → ℝ) (Dv : Vec d → Vec d) : Prop

Membership in H¹_{s,loc}(ℝ^d): on every centered Euclidean ball, a weak-gradient pair approximated by smooth functions in the H¹_s norm.

Equations

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

Weak solutions and the Liouville class

def HCPolySupport.HighContrast.IsWeakSolutionOn {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) (F : Vec d → Vec d) : Prop

The weak interior equation -∇·(b F) = 0 in V: against every smooth compactly supported test the flux pairing is absolutely convergent and vanishes. Absolute convergence is the well-formedness of the printed distributional display, and it is what keeps the equation from holding by the failure of the pairing.

Equations

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

def HCPolySupport.HighContrast.MemLiouvilleClass {d : ℕ} (b : CoeffField d) (ϑ : ℝ) (v : Vec d → ℝ) (Dv : Vec d → Vec d) : Prop

The Liouville class 𝒜_{1,ϑ}(ℝ^d) of e.random.liouville.growth. The growth condition is the vanishing-limit form of the limsup display, equivalent for the nonnegative normalized averages.

Equations

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

def HCPolySupport.HighContrast.MemAffineH10 {d : ℕ} (U : Set (Vec d)) (g₀ h : H1Function U) : Prop

Membership of h in the affine class g₀ + H¹₀(U), through an H10Function witness matching function and gradient a.e. on U.

Equations

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

Domains and their shape data

The domains carrying the Dirichlet estimate are the bounded convex domains of IsOpenBoundedConvexDomain, the domain class of the coarse-graining library. The geometric datum through which the endpoint constant is allowed to depend on the domain is the concentric ball sandwich of the adapted domain: an inner radius and an outer radius. For a convex body this pair plays exactly the role that the Lipschitz character plays for a Lipschitz domain — it controls the trace, extension and fractional Poincaré constants — and it is the convex reading of the domain dependence recorded at e.random.dirichlet.

def HCPolySupport.HighContrast.matImage {d : ℕ} (M : Mat d) (U : Set (Vec d)) : Set (Vec d)

The image of a set under a linear map, used for the adapted domain s_bar^{-1/2}U whose shape governs the endpoint constant.

Equations

• HCPolySupport.HighContrast.matImage M U = HCPolySupport.matVecMul M '' U

def HCPolySupport.HighContrast.HasBallSandwich {d : ℕ} (U : Set (Vec d)) (ρ Rad : ℝ) : Prop

U contains, and is contained in, concentric Euclidean balls of radii ρ and Rad. The pair (ρ, Rad) is the shape datum of a convex domain: an estimate whose constant depends on the domain only through (ρ, Rad) is uniform over every domain admitting that sandwich. The radii are signed constraints on the shape, so their sign is fixed here: a ball is read through the square of its radius, and without the sign conditions the same domain would be indexed by both a radius and its negative.

Equations

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