ExitMeanValueIdentificationCarrier

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The zero-trace carrier: Poincare inequality, ellipticity and the supremum bound

Three facts about the zero-trace value--gradient carrier are isolated here, all of them used by the identification of the vanishing-shift limit of the Dirichlet resolvents with a weak solution.

• ZeroTraceSobolev.exists_poincare_constant transports the zero-trace Poincare inequality of a bounded convex domain from honest zero-trace Sobolev functions to the graph carrier, using the realization theorem of the carrier on such domains.
• mul_norm_gradient_sq_le_coefficientPairing is the elliptic lower bound of the coefficient pairing on the carrier, read off the coercivity estimate of the shifted bilinear form at the shift equal to the lower ellipticity constant.
• norm_scalarL2_le_of_ae_bound converts an essential supremum bound into an L² bound on a bounded domain.

None of this is specific to the exhaustion cubes.

The Poincare inequality on the carrier

theorem DivergenceFormProcess.Form.ZeroTraceSobolev.exists_poincare_constant {d : ℕ} [NeZero d] {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (z : ZeroTraceSobolev U), ‖toL2 z‖ ≤ C * ‖gradient z‖

The zero-trace Poincare inequality on the graph carrier. On a bounded convex domain every element of the carrier is realized by an honest zero-trace Sobolev function, so the Poincare constant of the domain controls the value component by the gradient component.

Ellipticity of the coefficient pairing on the carrier

theorem DivergenceFormProcess.Form.coefficientPairing_gradient_eq_shiftedBilin {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {lam Lam : ℝ} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (u w : ZeroTraceSobolev U) : coefficientPairing a U (ZeroTraceSobolev.gradient u) (ZeroTraceSobolev.gradient w) = ((shiftedBilin hEll 0) u) w

The coefficient pairing of two carrier gradients is the value of the unshifted bilinear form.

theorem DivergenceFormProcess.Form.mul_norm_gradient_sq_le_coefficientPairing {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {lam Lam : ℝ} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (u : ZeroTraceSobolev U) : lam * ‖ZeroTraceSobolev.gradient u‖ ^ 2 ≤ coefficientPairing a U (ZeroTraceSobolev.gradient u) (ZeroTraceSobolev.gradient u)

The elliptic lower bound of the coefficient pairing on the carrier.

The supremum-to-L² bound

noncomputable def DivergenceFormProcess.Form.scalarL2Factor {d : ℕ} (U : Set (HCPolySupport.Vec d)) : ℝ

The factor converting an essential supremum bound into an L² bound on a domain.

Equations

• DivergenceFormProcess.Form.scalarL2Factor U = (MeasureTheory.volume U).toReal ^ 2⁻¹

theorem DivergenceFormProcess.Form.scalarL2Factor_nonneg {d : ℕ} (U : Set (HCPolySupport.Vec d)) : 0 ≤ scalarL2Factor U

theorem DivergenceFormProcess.Form.norm_scalarL2_le_of_ae_bound {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (F : ↥(HCPolySupport.ScalarL2 U)) {C : ℝ} (hC : 0 ≤ C) (hF : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |↑↑F x| ≤ C) : ‖F‖ ≤ scalarL2Factor U * C

An essential supremum bound on a bounded domain is an L² bound.