Documentation

def HCPolySupport.IsEssentiallyEllipticFieldOn {d : ℕ} (lam Lam : ℝ) (U : Set (Vec d)) (a : CoeffField d) :

Essential/a.e. ellipticity on a deterministic observation set.

This is the probability-facing version of IsEllipticFieldOn: the restricted coefficient field is measurable, but ellipticity is required only volumeMeasureOn U-almost everywhere. This is the legacy essential variant used by constructions that identify coefficient fields up to spatial a.e. agreement.

Equations

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

Instances For

def HCPolySupport.IsAEEllipticFieldOn {d : ℕ} (lam Lam : ℝ) (U : Set (Vec d)) (a : CoeffField d) :

Spatial a.e. ellipticity on a deterministic observation set, with only an a.e.-strongly-measurable coefficient representative.

This is the boundary-stable variant needed by Ch. 5: unlike IsEssentiallyEllipticFieldOn, it is insensitive to changing the coefficient field on a null boundary layer.

Equations

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

Instances For

def HCPolySupport.EssentialQuantitativeEllipticSlice {d : ℕ} (U : Set (Vec d)) (k : ℕ) (a : CoeffField d) :

The k-th essential quantitative ellipticity slice. Unlike QuantitativeEllipticSlice, this records the quantitative ellipticity bounds only a.e. on U, matching the probability sigma lane generated by local integral tests.

Equations

HCPolySupport.EssentialQuantitativeEllipticSlice U k a = HCPolySupport.IsEssentiallyEllipticFieldOn (↑k + 1)⁻¹ (↑k + 1) U a

Instances For

def HCPolySupport.AEEQuantitativeEllipticSlice {d : ℕ} (U : Set (Vec d)) (k : ℕ) (a : CoeffField d) :

The k-th quantitative slice for the boundary-stable spatial-a.e. ellipticity predicate. This is the countable version of IsAEEllipticFieldOn, intended for law-relative Chapter 4/5 plumbing where only a.e.-strong measurability is available.

Equations

HCPolySupport.AEEQuantitativeEllipticSlice U k a = HCPolySupport.IsAEEllipticFieldOn (↑k + 1)⁻¹ (↑k + 1) U a

Instances For

theorem HCPolySupport.IsEllipticFieldOn.translateSet_of_translateCoeffField {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (z : Vec d) (hEll : IsEllipticFieldOn lam Lam U (translateCoeffField z a)) :

IsEllipticFieldOn lam Lam (translateSet z U) a

Transport pointwise ellipticity of the translated coefficient field on U back to pointwise ellipticity of the original coefficient field on the translated set. The a.e. Ch5 law-data lane uses this only as a deterministic translation step before weakening to IsAEEllipticFieldOn; it does not add any quantitative ellipticity input beyond the original constants.

theorem HCPolySupport.IsEssentiallyEllipticFieldOn.measurableSet {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (h : IsEssentiallyEllipticFieldOn lam Lam U a) :

theorem HCPolySupport.IsEssentiallyEllipticFieldOn.ae_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (h : IsEssentiallyEllipticFieldOn lam Lam U a) :

∀ᵐ (x : Vec d) ∂volumeMeasureOn U, IsEllipticMatrix lam Lam (a x)

theorem HCPolySupport.IsEssentiallyEllipticFieldOn.of_isEllipticFieldOn {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (h : IsEllipticFieldOn lam Lam U a) :

IsEssentiallyEllipticFieldOn lam Lam U a

theorem HCPolySupport.IsEssentiallyEllipticFieldOn.mono_constants {d : ℕ} {lam Lam lam' Lam' : ℝ} {U : Set (Vec d)} {a : CoeffField d} (h : IsEssentiallyEllipticFieldOn lam Lam U a) (hlam'_pos : 0 < lam') (hlam'_le : lam' ≤ lam) (hLam_le : Lam ≤ Lam') :

IsEssentiallyEllipticFieldOn lam' Lam' U a

theorem HCPolySupport.IsAEEllipticFieldOn.measurableSet {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (h : IsAEEllipticFieldOn lam Lam U a) :

theorem HCPolySupport.IsAEEllipticFieldOn.aestronglyMeasurable_restrictCoeffField_apply {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (h : IsAEEllipticFieldOn lam Lam U a) (i j : Fin d) :

MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => restrictCoeffField U a x i j) (volumeMeasureOn U)

theorem HCPolySupport.IsAEEllipticFieldOn.ae_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (h : IsAEEllipticFieldOn lam Lam U a) :

∀ᵐ (x : Vec d) ∂volumeMeasureOn U, IsEllipticMatrix lam Lam (a x)

theorem HCPolySupport.IsAEEllipticFieldOn.of_isEssentiallyEllipticFieldOn {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (h : IsEssentiallyEllipticFieldOn lam Lam U a) :

IsAEEllipticFieldOn lam Lam U a

theorem HCPolySupport.IsAEEllipticFieldOn.of_isEllipticFieldOn {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (h : IsEllipticFieldOn lam Lam U a) :

IsAEEllipticFieldOn lam Lam U a

theorem HCPolySupport.IsAEEllipticFieldOn.mono_constants {d : ℕ} {lam Lam lam' Lam' : ℝ} {U : Set (Vec d)} {a : CoeffField d} (h : IsAEEllipticFieldOn lam Lam U a) (hlam'_pos : 0 < lam') (hlam'_le : lam' ≤ lam) (hLam_le : Lam ≤ Lam') :

IsAEEllipticFieldOn lam' Lam' U a

theorem HCPolySupport.IsAEEllipticFieldOn.mono {d : ℕ} {lam Lam : ℝ} {U V : Set (Vec d)} {a : CoeffField d} (h : IsAEEllipticFieldOn lam Lam U a) (hV : MeasurableSet V) (hVU : V ⊆ U) :

IsAEEllipticFieldOn lam Lam V a

theorem HCPolySupport.IsAEEllipticFieldOn.biUnion_finset {d : ℕ} {ι : Type u_1} {lam Lam : ℝ} (s : Finset ι) {U : ι → Set (Vec d)} {a : CoeffField d} (h : ∀ i ∈ s, IsAEEllipticFieldOn lam Lam (U i) a) :

IsAEEllipticFieldOn lam Lam (⋃ i ∈ s, U i) a

Finite unions preserve spatial a.e. ellipticity when the same quantitative constants work on every member of the finite family.

theorem HCPolySupport.IsAEEllipticFieldOn.exists_biUnion_finset {d : ℕ} {ι : Type u_1} (s : Finset ι) (hs : s.Nonempty) {U : ι → Set (Vec d)} {a : CoeffField d} (h : ∀ i ∈ s, ∃ (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ IsAEEllipticFieldOn lam Lam (U i) a) :

∃ (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ IsAEEllipticFieldOn lam Lam (⋃ i ∈ s, U i) a

Finite unions preserve spatial a.e. ellipticity with explicit combined constants: the lower constant is the finite infimum of the local lower constants, and the upper constant is the finite supremum of the local upper constants.

theorem HCPolySupport.IsAEEllipticFieldOn.translateSet_of_translateCoeffField {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (z : Vec d) (h : IsAEEllipticFieldOn lam Lam U (translateCoeffField z a)) :

IsAEEllipticFieldOn lam Lam (translateSet z U) a

theorem HCPolySupport.IsAEEllipticFieldOn.memVectorL2_matVecMul {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a : CoeffField d} (h : IsAEEllipticFieldOn lam Lam U a) {f : Vec d → Vec d} (hf : MemVectorL2 U f) :

MemVectorL2 U fun (x : Vec d) => matVecMul (a x) (f x)

theorem HCPolySupport.IsAEEllipticFieldOn.cubeSet_of_openCubeSet {d : ℕ} {lam Lam : ℝ} {Q : TriadicCube d} {a : CoeffField d} (h : IsAEEllipticFieldOn lam Lam (openCubeSet Q) a) :

IsAEEllipticFieldOn lam Lam (cubeSet Q) a

Spatial a.e. ellipticity on the open core of a triadic cube extends to the half-open cube, since the two restricted volume measures agree.

theorem HCPolySupport.IsAEEllipticFieldOn.cubeSet_of_isEllipticFieldOn_openCubeSet {d : ℕ} {lam Lam : ℝ} {Q : TriadicCube d} {a : CoeffField d} (h : IsEllipticFieldOn lam Lam (openCubeSet Q) a) :

IsAEEllipticFieldOn lam Lam (cubeSet Q) a

theorem HCPolySupport.IsAEEllipticFieldOn.cubeSet_originCube_of_isEllipticFieldOn_openCubeSet_originCube {d : ℕ} {lam Lam : ℝ} {n : ℤ} {a : CoeffField d} (h : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) :

IsAEEllipticFieldOn lam Lam (cubeSet (originCube d n)) a

theorem HCPolySupport.IsAEEllipticFieldOn.of_localAgreementOn {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a b : CoeffField d} (hab : LocalAgreementOn U a b) (h : IsAEEllipticFieldOn lam Lam U a) :

IsAEEllipticFieldOn lam Lam U b

theorem HCPolySupport.IsAEEllipticFieldOn.iff_of_localAgreementOn {d : ℕ} {lam Lam : ℝ} {U : Set (Vec d)} {a b : CoeffField d} (hab : LocalAgreementOn U a b) :

IsAEEllipticFieldOn lam Lam U a ↔ IsAEEllipticFieldOn lam Lam U b

theorem HCPolySupport.IsAEEllipticFieldOn.measurableSet_localSigma {d : ℕ} (lam Lam : ℝ) (U : Set (Vec d)) :

MeasurableSet {a : CoeffField d | IsAEEllipticFieldOn lam Lam U a}

theorem HCPolySupport.QuantitativeEllipticSlice.mono {d : ℕ} {U V : Set (Vec d)} {k : ℕ} {a : CoeffField d} (h : QuantitativeEllipticSlice U k a) (hV : MeasurableSet V) (hVU : V ⊆ U) :

QuantitativeEllipticSlice V k a

theorem HCPolySupport.QuantitativeEllipticSlice.eqOn_saturated_of_measurableSet_localSigma {d : ℕ} {U : Set (Vec d)} {k : ℕ} {a b : CoeffField d} (hmeas : MeasurableSet {c : CoeffField d | QuantitativeEllipticSlice U k c}) (h : ∀ x ∈ U, a x = b x) :

QuantitativeEllipticSlice U k a ↔ QuantitativeEllipticSlice U k b

A raw pointwise quantitative slice set can be PointwiseLocalSigma U-measurable only if membership in that slice is invariant under pointwise changes outside U. This records the exact compatibility condition imposed by the local coefficient-field sigma algebra.

@[reducible, inline]

abbrev HCPolySupport.QuantitativeEllipticSlice.localMeasurableSpace {d : ℕ} (U : Set (Vec d)) (k : ℕ) :

MeasurableSpace { a : CoeffField d // QuantitativeEllipticSlice U k a }

The subtype sigma algebra inherited from the local coefficient-field sigma algebra. We keep this as an explicit definition, rather than an instance, so theorem statements choose the local lane deliberately.

Equations

HCPolySupport.QuantitativeEllipticSlice.localMeasurableSpace U k = MeasurableSpace.comap Subtype.val (HCPolySupport.PointwiseLocalSigma U)

Instances For

theorem HCPolySupport.QuantitativeEllipticSlice.measurable_val_localMeasurableSpace {d : ℕ} {U : Set (Vec d)} {k : ℕ} :

Measurable Subtype.val

theorem HCPolySupport.QuantitativeEllipticSlice.memLp_restrictCoeffField {d : ℕ} {U : Set (Vec d)} {k : ℕ} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (h : QuantitativeEllipticSlice U k a) :

MeasureTheory.MemLp (fun (x : Vec d) (i j : Fin d) => restrictCoeffField U a x i j) 2 (volumeMeasureOn U)

noncomputable def HCPolySupport.QuantitativeEllipticSlice.toMatrixL2 {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) :

↥(MeasureTheory.Lp (Fin d → Fin d → ℝ) 2 (volumeMeasureOn U))

The matrix-valued L² class of the coefficient field restricted to U on a quantitative ellipticity slice.

Equations

HCPolySupport.QuantitativeEllipticSlice.toMatrixL2 a = MeasureTheory.MemLp.toLp (fun (x : HCPolySupport.Vec d) (i j : Fin d) => HCPolySupport.restrictCoeffField U (↑a) x i j) ⋯

Instances For

theorem HCPolySupport.QuantitativeEllipticSlice.memLp_hilbertMatrix_restrictCoeffField {d : ℕ} {U : Set (Vec d)} {k : ℕ} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (h : QuantitativeEllipticSlice U k a) :

MeasureTheory.MemLp (fun (x : Vec d) => HilbertMat.ofMat (restrictCoeffField U a x)) 2 (volumeMeasureOn U)

noncomputable def HCPolySupport.QuantitativeEllipticSlice.toHilbertMatrixL2 {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) :

↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U))

The Hilbert-matrix-valued L² class of the coefficient field restricted to U on a quantitative ellipticity slice.

Equations

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

Instances For

Measurable toHilbertMatrixL2

theorem HCPolySupport.QuantitativeEllipticSlice.measurable_toHilbertMatrixL2_of_norm_eq_iSup_abs_inner {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : ℕ → ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U))) (hu : DenseRange u) (hNormEq : ∀ (f : ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U))), ‖f‖ = ⨆ (n : ℕ), |inner ℝ (u n) f|) (hInner : ∀ (n : ℕ), Measurable fun (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) => inner ℝ (u n) (toHilbertMatrixL2 a)) :

Strong Borel measurability of the coefficient-field L² realization follows from a countable probe family that both separates the Hilbert norm and has measurable scalar coordinates on the local slice sigma algebra.

Measurable toHilbertMatrixL2

theorem HCPolySupport.QuantitativeEllipticSlice.measurable_toHilbertMatrixL2_of_dense_inner {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : ℕ → ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U))) (hu : DenseRange u) (hInner : ∀ (n : ℕ), Measurable fun (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) => inner ℝ (u n) (toHilbertMatrixL2 a)) :

Strong Borel measurability of the coefficient-field L² realization follows from measurable scalar coordinates against any dense probe sequence in the Hilbert L² target. This is the non-circular endpoint used by the fixed-competitor measurability cleanup.

theorem HCPolySupport.QuantitativeEllipticSlice.coeFn_toMatrixL2 {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) :

↑↑(toMatrixL2 a) =ᵐ[volumeMeasureOn U] fun (x : Vec d) (i j : Fin d) => restrictCoeffField U (↑a) x i j

theorem HCPolySupport.QuantitativeEllipticSlice.coeFn_toHilbertMatrixL2 {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) :

↑↑(toHilbertMatrixL2 a) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => HilbertMat.ofMat (restrictCoeffField U (↑a) x)

noncomputable def HCPolySupport.QuantitativeEllipticSlice.matrixL2Entry {d : ℕ} {U : Set (Vec d)} (i j : Fin d) :

↥(MeasureTheory.Lp (Fin d → Fin d → ℝ) 2 (volumeMeasureOn U)) →L[ℝ ] ↥(ScalarL2 U)

The continuous linear extraction of matrix entry (i, j) from a matrix-valued L² class.

Equations

HCPolySupport.QuantitativeEllipticSlice.matrixL2Entry i j = ContinuousLinearMap.compLpL 2 (HCPolySupport.volumeMeasureOn U) (ContinuousLinearMap.proj j ∘SL ContinuousLinearMap.proj i)

Instances For

noncomputable def HCPolySupport.QuantitativeEllipticSlice.hilbertMatrixL2Entry {d : ℕ} {U : Set (Vec d)} (i j : Fin d) :

↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U)) →L[ℝ ] ↥(ScalarL2 U)

The continuous linear extraction of entry (i, j) from a Hilbert-matrix-valued L² class.

Equations

HCPolySupport.QuantitativeEllipticSlice.hilbertMatrixL2Entry i j = ContinuousLinearMap.compLpL 2 (HCPolySupport.volumeMeasureOn U) (HCPolySupport.HilbertMat.entryL i j)

Instances For

theorem HCPolySupport.QuantitativeEllipticSlice.coeFn_matrixL2Entry_toMatrixL2 {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (i j : Fin d) (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) :

↑↑((matrixL2Entry i j) (toMatrixL2 a)) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => restrictCoeffField U (↑a) x i j

theorem HCPolySupport.QuantitativeEllipticSlice.coeFn_hilbertMatrixL2Entry_toHilbertMatrixL2 {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (i j : Fin d) (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) :

↑↑((hilbertMatrixL2Entry i j) (toHilbertMatrixL2 a)) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => restrictCoeffField U (↑a) x i j

theorem HCPolySupport.QuantitativeEllipticSlice.inner_toScalarL2_matrixL2Entry_toMatrixL2_eq_setIntegral {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {w : Vec d → ℝ} (hw : MemScalarL2 U w) (i j : Fin d) (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) :

inner ℝ (toScalarL2 hw) ((matrixL2Entry i j) (toMatrixL2 a)) = ∫ (x : Vec d) in U, w x * ↑a x i j

theorem HCPolySupport.QuantitativeEllipticSlice.inner_scalarL2_matrixEntry_eq_setIntegral {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {w : Vec d → ℝ} (hw : MemScalarL2 U w) (i j : Fin d) (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) :

inner ℝ (toScalarL2 hw) ((hilbertMatrixL2Entry i j) (toHilbertMatrixL2 a)) = ∫ (x : Vec d) in U, w x * ↑a x i j

theorem HCPolySupport.QuantitativeEllipticSlice.memScalarL2_hilbertMatrix_entry_of_memLp {d : ℕ} {U : Set (Vec d)} {g : Vec d → HilbertMat d} (hg : MeasureTheory.MemLp g 2 (volumeMeasureOn U)) (i j : Fin d) :

MemScalarL2 U fun (x : Vec d) => (HilbertMat.entryL i j) (g x)

theorem HCPolySupport.QuantitativeEllipticSlice.inner_toScalarL2_hilbertMatrixL2Entry_eq_integral {d : ℕ} {U : Set (Vec d)} {w : Vec d → ℝ} (hw : MemScalarL2 U w) (i j : Fin d) (A : ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U))) :

inner ℝ (toScalarL2 hw) ((hilbertMatrixL2Entry i j) A) = ∫ (x : Vec d), w x * ((↑↑A x).ofLp i).ofLp j ∂volumeMeasureOn U

theorem HCPolySupport.QuantitativeEllipticSlice.integrable_hilbertMatrix_entry_mul {d : ℕ} {U : Set (Vec d)} {g : Vec d → HilbertMat d} (hg : MeasureTheory.MemLp g 2 (volumeMeasureOn U)) (A : ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U))) (i j : Fin d) :

MeasureTheory.Integrable (fun (x : Vec d) => ((g x).ofLp i).ofLp j * ((↑↑A x).ofLp i).ofLp j) (volumeMeasureOn U)

theorem HCPolySupport.QuantitativeEllipticSlice.integrable_hilbertMatrix_entry_sum {d : ℕ} {U : Set (Vec d)} {g : Vec d → HilbertMat d} (hg : MeasureTheory.MemLp g 2 (volumeMeasureOn U)) (A : ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U))) (i : Fin d) :

MeasureTheory.Integrable (fun (x : Vec d) => ∑ j : Fin d, ((g x).ofLp i).ofLp j * ((↑↑A x).ofLp i).ofLp j) (volumeMeasureOn U)

theorem HCPolySupport.QuantitativeEllipticSlice.inner_hilbertMatrixL2_eq_sum_entry_inner {d : ℕ} {U : Set (Vec d)} {g : Vec d → HilbertMat d} (hg : MeasureTheory.MemLp g 2 (volumeMeasureOn U)) (A : ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U))) :

inner ℝ (MeasureTheory.MemLp.toLp g hg) A = ∑ i : Fin d, ∑ j : Fin d, inner ℝ (toScalarL2 ⋯) ((hilbertMatrixL2Entry i j) A)

theorem HCPolySupport.QuantitativeEllipticSlice.exists_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {ε : ℝ} (hε_pos : 0 < ε) (hEll : IsEllipticFieldOn ε ε⁻¹ U a) :

∃ (k : ℕ), QuantitativeEllipticSlice U k a

Any positive quantitative ellipticity constants can be relaxed to one of the countable natural-number slices.

theorem HCPolySupport.EssentialQuantitativeEllipticSlice.of_quantitative {d : ℕ} {U : Set (Vec d)} {k : ℕ} {a : CoeffField d} (h : QuantitativeEllipticSlice U k a) :

EssentialQuantitativeEllipticSlice U k a

@[reducible, inline]

abbrev HCPolySupport.EssentialQuantitativeEllipticSlice.localMeasurableSpace {d : ℕ} (U : Set (Vec d)) (k : ℕ) :

MeasurableSpace { a : CoeffField d // EssentialQuantitativeEllipticSlice U k a }

The subtype sigma algebra inherited from the local coefficient-field sigma algebra, now for essential/a.e. quantitative slices.

Equations

HCPolySupport.EssentialQuantitativeEllipticSlice.localMeasurableSpace U k = MeasurableSpace.comap Subtype.val (HCPolySupport.PointwiseLocalSigma U)

Instances For

theorem HCPolySupport.EssentialQuantitativeEllipticSlice.measurable_val_localMeasurableSpace {d : ℕ} {U : Set (Vec d)} {k : ℕ} :

Measurable Subtype.val

theorem HCPolySupport.EssentialQuantitativeEllipticSlice.measurableSet {d : ℕ} {U : Set (Vec d)} {k : ℕ} {a : CoeffField d} (h : EssentialQuantitativeEllipticSlice U k a) :

theorem HCPolySupport.EssentialQuantitativeEllipticSlice.ae_isEllipticMatrix {d : ℕ} {U : Set (Vec d)} {k : ℕ} {a : CoeffField d} (h : EssentialQuantitativeEllipticSlice U k a) :

∀ᵐ (x : Vec d) ∂volumeMeasureOn U, IsEllipticMatrix (↑k + 1)⁻¹ (↑k + 1) (a x)

theorem HCPolySupport.EssentialQuantitativeEllipticSlice.memLp_restrictCoeffField {d : ℕ} {U : Set (Vec d)} {k : ℕ} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (h : EssentialQuantitativeEllipticSlice U k a) :

MeasureTheory.MemLp (fun (x : Vec d) (i j : Fin d) => restrictCoeffField U a x i j) 2 (volumeMeasureOn U)

theorem HCPolySupport.EssentialQuantitativeEllipticSlice.memLp_hilbertMatrix_restrictCoeffField {d : ℕ} {U : Set (Vec d)} {k : ℕ} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (h : EssentialQuantitativeEllipticSlice U k a) :

MeasureTheory.MemLp (fun (x : Vec d) => HilbertMat.ofMat (restrictCoeffField U a x)) 2 (volumeMeasureOn U)

noncomputable def HCPolySupport.EssentialQuantitativeEllipticSlice.toHilbertMatrixL2 {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (a : { a : CoeffField d // EssentialQuantitativeEllipticSlice U k a }) :

↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U))

The Hilbert-matrix-valued L² class of the restricted coefficient field on an essential quantitative ellipticity slice.

Equations

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

Instances For

theorem HCPolySupport.EssentialQuantitativeEllipticSlice.coeFn_toHilbertMatrixL2 {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (a : { a : CoeffField d // EssentialQuantitativeEllipticSlice U k a }) :

↑↑(toHilbertMatrixL2 a) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => HilbertMat.ofMat (restrictCoeffField U (↑a) x)

theorem HCPolySupport.EssentialQuantitativeEllipticSlice.exists_of_isEssentiallyEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {ε : ℝ} (hε_pos : 0 < ε) (hEll : IsEssentiallyEllipticFieldOn ε ε⁻¹ U a) :

∃ (k : ℕ), EssentialQuantitativeEllipticSlice U k a

Any positive essential ellipticity constants can be relaxed to one of the countable essential natural-number slices.

@[reducible, inline]

abbrev HCPolySupport.AEEQuantitativeEllipticSlice.localMeasurableSpace {d : ℕ} (U : Set (Vec d)) (k : ℕ) :

MeasurableSpace { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }

The subtype sigma algebra inherited from the local coefficient-field sigma algebra, for the boundary-stable AEE quantitative slices.

Equations

HCPolySupport.AEEQuantitativeEllipticSlice.localMeasurableSpace U k = MeasurableSpace.comap Subtype.val (HCPolySupport.PointwiseLocalSigma U)

Instances For

theorem HCPolySupport.AEEQuantitativeEllipticSlice.measurable_val_localMeasurableSpace {d : ℕ} {U : Set (Vec d)} {k : ℕ} :

Measurable Subtype.val

theorem HCPolySupport.AEEQuantitativeEllipticSlice.measurableSet {d : ℕ} {U : Set (Vec d)} {k : ℕ} {a : CoeffField d} (h : AEEQuantitativeEllipticSlice U k a) :

theorem HCPolySupport.AEEQuantitativeEllipticSlice.aestronglyMeasurable_restrictCoeffField_apply {d : ℕ} {U : Set (Vec d)} {k : ℕ} {a : CoeffField d} (h : AEEQuantitativeEllipticSlice U k a) (i j : Fin d) :

MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => restrictCoeffField U a x i j) (volumeMeasureOn U)

theorem HCPolySupport.AEEQuantitativeEllipticSlice.ae_isEllipticMatrix {d : ℕ} {U : Set (Vec d)} {k : ℕ} {a : CoeffField d} (h : AEEQuantitativeEllipticSlice U k a) :

∀ᵐ (x : Vec d) ∂volumeMeasureOn U, IsEllipticMatrix (↑k + 1)⁻¹ (↑k + 1) (a x)

theorem HCPolySupport.AEEQuantitativeEllipticSlice.of_localAgreementOn {d : ℕ} {U : Set (Vec d)} {k : ℕ} {a b : CoeffField d} (hab : LocalAgreementOn U a b) (h : AEEQuantitativeEllipticSlice U k a) :

AEEQuantitativeEllipticSlice U k b

theorem HCPolySupport.AEEQuantitativeEllipticSlice.iff_of_localAgreementOn {d : ℕ} {U : Set (Vec d)} {k : ℕ} {a b : CoeffField d} (hab : LocalAgreementOn U a b) :

AEEQuantitativeEllipticSlice U k a ↔ AEEQuantitativeEllipticSlice U k b

theorem HCPolySupport.AEEQuantitativeEllipticSlice.measurableSet_localSigma {d : ℕ} (U : Set (Vec d)) (k : ℕ) :

MeasurableSet {a : CoeffField d | AEEQuantitativeEllipticSlice U k a}

theorem HCPolySupport.AEEQuantitativeEllipticSlice.memLp_restrictCoeffField {d : ℕ} {U : Set (Vec d)} {k : ℕ} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (h : AEEQuantitativeEllipticSlice U k a) :

MeasureTheory.MemLp (fun (x : Vec d) (i j : Fin d) => restrictCoeffField U a x i j) 2 (volumeMeasureOn U)

AEE quantitative slices still give an L² coefficient realization: the coordinate functions are only a.e.-strongly measurable, but the quantitative ellipticity bound supplies the uniform L² estimate.

theorem HCPolySupport.AEEQuantitativeEllipticSlice.memLp_hilbertMatrix_restrictCoeffField {d : ℕ} {U : Set (Vec d)} {k : ℕ} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (h : AEEQuantitativeEllipticSlice U k a) :

MeasureTheory.MemLp (fun (x : Vec d) => HilbertMat.ofMat (restrictCoeffField U a x)) 2 (volumeMeasureOn U)

noncomputable def HCPolySupport.AEEQuantitativeEllipticSlice.toHilbertMatrixL2 {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) :

↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U))

The Hilbert-matrix-valued L² class of the restricted coefficient field on a spatial almost-everywhere quantitative ellipticity slice.

Equations

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

Instances For

theorem HCPolySupport.AEEQuantitativeEllipticSlice.coeFn_toHilbertMatrixL2 {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) :

↑↑(toHilbertMatrixL2 a) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => HilbertMat.ofMat (restrictCoeffField U (↑a) x)

theorem HCPolySupport.AEEQuantitativeEllipticSlice.exists_of_aeeEllipticOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hlam_pos : 0 < lam) (hEll : IsAEEllipticFieldOn lam Lam U a) :

∃ (k : ℕ), AEEQuantitativeEllipticSlice U k a

Any positive spatial-a.e. ellipticity constants can be relaxed to one of the countable AEE quantitative slices.

theorem HCPolySupport.IsLocallyUniformlyElliptic.exists_isEllipticFieldOn_of_subset_closedBall {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {R : ℝ} (hloc : IsLocallyUniformlyElliptic a) (hR : 1 ≤ R) (hU : MeasurableSet U) (hsub : U ⊆ Metric.closedBall 0 R) :

∃ (ε : ℝ), 0 < ε ∧ ε ≤ 1 ∧ IsEllipticFieldOn ε ε⁻¹ U a

Restrict local uniform ellipticity from a centered closed ball to a measurable subset of that ball.

theorem HCPolySupport.IsLocallyUniformlyElliptic.exists_isEllipticFieldOn_cubeSet_originCube {d : ℕ} {a : CoeffField d} (hloc : IsLocallyUniformlyElliptic a) (n : ℤ) :

∃ (ε : ℝ), 0 < ε ∧ ε ≤ 1 ∧ IsEllipticFieldOn ε ε⁻¹ (cubeSet (originCube d n)) a

theorem HCPolySupport.IsLocallyUniformlyElliptic.exists_isEllipticFieldOn_openCubeSet_originCube {d : ℕ} {a : CoeffField d} (hloc : IsLocallyUniformlyElliptic a) (n : ℤ) :

∃ (ε : ℝ), 0 < ε ∧ ε ≤ 1 ∧ IsEllipticFieldOn ε ε⁻¹ (openCubeSet (originCube d n)) a

theorem HCPolySupport.IsLocallyUniformlyElliptic.exists_quantitativeEllipticSlice_cubeSet_originCube {d : ℕ} {a : CoeffField d} (hloc : IsLocallyUniformlyElliptic a) (n : ℤ) :

∃ (k : ℕ), QuantitativeEllipticSlice (cubeSet (originCube d n)) k a

theorem HCPolySupport.IsLocallyUniformlyElliptic.exists_quantitativeEllipticSlice_openCubeSet_originCube {d : ℕ} {a : CoeffField d} (hloc : IsLocallyUniformlyElliptic a) (n : ℤ) :

∃ (k : ℕ), QuantitativeEllipticSlice (openCubeSet (originCube d n)) k a

theorem HCPolySupport.IsLocallyUniformlyElliptic.exists_essentialQuantitativeEllipticSlice_cubeSet_originCube {d : ℕ} {a : CoeffField d} (hloc : IsLocallyUniformlyElliptic a) (n : ℤ) :

∃ (k : ℕ), EssentialQuantitativeEllipticSlice (cubeSet (originCube d n)) k a

theorem HCPolySupport.IsLocallyUniformlyElliptic.exists_essentialQuantitativeEllipticSlice_openCubeSet_originCube {d : ℕ} {a : CoeffField d} (hloc : IsLocallyUniformlyElliptic a) (n : ℤ) :

∃ (k : ℕ), EssentialQuantitativeEllipticSlice (openCubeSet (originCube d n)) k a

theorem HCPolySupport.ae_exists_quantitativeEllipticSlice_cubeSet_originCube {d : ℕ} {P : MeasureTheory.Measure (CoeffField d)} (hloc : ∀ᵐ (a : CoeffField d) ∂P, IsLocallyUniformlyElliptic a) (n : ℤ) :

∀ᵐ (a : CoeffField d) ∂P, ∃ (k : ℕ), QuantitativeEllipticSlice (cubeSet (originCube d n)) k a

theorem HCPolySupport.ae_exists_quantitativeEllipticSlice_openCubeSet_originCube {d : ℕ} {P : MeasureTheory.Measure (CoeffField d)} (hloc : ∀ᵐ (a : CoeffField d) ∂P, IsLocallyUniformlyElliptic a) (n : ℤ) :

∀ᵐ (a : CoeffField d) ∂P, ∃ (k : ℕ), QuantitativeEllipticSlice (openCubeSet (originCube d n)) k a

theorem HCPolySupport.ae_exists_essentialQuantitativeEllipticSlice_cubeSet_originCube {d : ℕ} {P : MeasureTheory.Measure (CoeffField d)} (hloc : ∀ᵐ (a : CoeffField d) ∂P, IsLocallyUniformlyElliptic a) (n : ℤ) :

∀ᵐ (a : CoeffField d) ∂P, ∃ (k : ℕ), EssentialQuantitativeEllipticSlice (cubeSet (originCube d n)) k a

theorem HCPolySupport.ae_exists_essentialQuantitativeEllipticSlice_openCubeSet_originCube {d : ℕ} {P : MeasureTheory.Measure (CoeffField d)} (hloc : ∀ᵐ (a : CoeffField d) ∂P, IsLocallyUniformlyElliptic a) (n : ℤ) :

∀ᵐ (a : CoeffField d) ∂P, ∃ (k : ℕ), EssentialQuantitativeEllipticSlice (openCubeSet (originCube d n)) k a

noncomputable def HCPolySupport.quantitativeEllipticSliceIndex {Ω : Type u_1} {d : ℕ} (U : Set (Vec d)) (A : Ω → CoeffField d) (hcover : ∀ (ω : Ω), ∃ (k : ℕ), QuantitativeEllipticSlice U k (A ω)) :

Ω → ℕ

The least quantitative slice index selected from a total countable slice-cover proof. This is intentionally just the measurable-selection bookkeeping; proving that raw slice membership sets are measurable is a separate input.

Equations

HCPolySupport.quantitativeEllipticSliceIndex U A hcover ω = Nat.find ⋯

Instances For

theorem HCPolySupport.quantitativeEllipticSliceIndex_spec {Ω : Type u_1} {d : ℕ} (U : Set (Vec d)) (A : Ω → CoeffField d) (hcover : ∀ (ω : Ω), ∃ (k : ℕ), QuantitativeEllipticSlice U k (A ω)) (ω : Ω) :

QuantitativeEllipticSlice U (quantitativeEllipticSliceIndex U A hcover ω) (A ω)

theorem HCPolySupport.measurable_quantitativeEllipticSliceIndex_of_measurableSet {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (U : Set (Vec d)) (A : Ω → CoeffField d) (hcover : ∀ (ω : Ω), ∃ (k : ℕ), QuantitativeEllipticSlice U k (A ω)) (hSliceMeas : ∀ (k : ℕ), MeasurableSet {ω : Ω | QuantitativeEllipticSlice U k (A ω)}) :

Measurable (quantitativeEllipticSliceIndex U A hcover)

noncomputable def HCPolySupport.essentialQuantitativeEllipticSliceIndex {Ω : Type u_1} {d : ℕ} (U : Set (Vec d)) (A : Ω → CoeffField d) (hcover : ∀ (ω : Ω), ∃ (k : ℕ), EssentialQuantitativeEllipticSlice U k (A ω)) :

Ω → ℕ

The least essential quantitative slice index selected from a total countable cover. This is the a.e.-elliptic replacement for quantitativeEllipticSliceIndex in the probability handoff.

Equations

HCPolySupport.essentialQuantitativeEllipticSliceIndex U A hcover ω = Nat.find ⋯

Instances For

theorem HCPolySupport.essentialQuantitativeEllipticSliceIndex_spec {Ω : Type u_1} {d : ℕ} (U : Set (Vec d)) (A : Ω → CoeffField d) (hcover : ∀ (ω : Ω), ∃ (k : ℕ), EssentialQuantitativeEllipticSlice U k (A ω)) (ω : Ω) :

EssentialQuantitativeEllipticSlice U (essentialQuantitativeEllipticSliceIndex U A hcover ω) (A ω)

theorem HCPolySupport.measurable_essentialQuantitativeEllipticSliceIndex_of_measurableSet {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (U : Set (Vec d)) (A : Ω → CoeffField d) (hcover : ∀ (ω : Ω), ∃ (k : ℕ), EssentialQuantitativeEllipticSlice U k (A ω)) (hSliceMeas : ∀ (k : ℕ), MeasurableSet {ω : Ω | EssentialQuantitativeEllipticSlice U k (A ω)}) :

Measurable (essentialQuantitativeEllipticSliceIndex U A hcover)

noncomputable def HCPolySupport.aeeQuantitativeEllipticSliceIndex {Ω : Type u_1} {d : ℕ} (U : Set (Vec d)) (A : Ω → CoeffField d) (hcover : ∀ (ω : Ω), ∃ (k : ℕ), AEEQuantitativeEllipticSlice U k (A ω)) :

Ω → ℕ

The least AEE quantitative slice index selected from a total countable cover. This is the boundary-stable analogue of essentialQuantitativeEllipticSliceIndex; applications to Chapter 4 laws first restrict to the full-measure support on which the cover is available.

Equations

HCPolySupport.aeeQuantitativeEllipticSliceIndex U A hcover ω = Nat.find ⋯

Instances For

theorem HCPolySupport.aeeQuantitativeEllipticSliceIndex_spec {Ω : Type u_1} {d : ℕ} (U : Set (Vec d)) (A : Ω → CoeffField d) (hcover : ∀ (ω : Ω), ∃ (k : ℕ), AEEQuantitativeEllipticSlice U k (A ω)) (ω : Ω) :

AEEQuantitativeEllipticSlice U (aeeQuantitativeEllipticSliceIndex U A hcover ω) (A ω)