Documentation

LeanPool.Superdiffusion.Algsuperdiff.StochasticProcess.Common.DivergenceForm.PartDomainTransport

PartDomainTransport #

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

Transport between nested domains #

This module records scalar restriction, zero extension for zero-trace Sobolev elements, and the pairing identities used to move weak formulations between nested domains.

source
theorem DivergenceFormProcess.Form.coefficientPairing_eq_integral_inner {d : ℕ} (a : HCPolySupport.CoeffField d) (W : Set (HCPolySupport.Vec d)) (F G : ↥(HCPolySupport.HilbertVectorL2 W)) :
coefficientPairing a W F G = ∫ (x : HCPolySupport.Vec d) in W, inner ℝ ((HCPolySupport.HilbertVec.applyMat (a x)) (↑↑F x)) (↑↑G x)

The coefficient pairing is the integral of the pointwise inner product of the coefficient image of the first field against the second.

source
theorem DivergenceFormProcess.Form.scalar_inner_zeroExtension_eq_restriction {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (hV : MeasurableSet V) (hU : MeasurableSet U) (hVU : V ⊆ U) (zU : ↥(HCPolySupport.ScalarL2 U)) (zV : ↥(HCPolySupport.ScalarL2 V)) (φU : ↥(HCPolySupport.ScalarL2 U)) (φV : ↥(HCPolySupport.ScalarL2 V)) (hz : ↑↑zU =ᵐ[HCPolySupport.volumeMeasureOn U] V.indicator fun (x : HCPolySupport.Vec d) => ↑↑zV x) (hφ : ↑↑φV =ᵐ[HCPolySupport.volumeMeasureOn V] ↑↑φU) :
inner ℝ zU φU = inner ℝ zV φV
source
theorem DivergenceFormProcess.Form.coefficientPairing_zeroExtension_eq_restriction {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hV : MeasurableSet V) (hU : MeasurableSet U) (hVU : V ⊆ U) (FU : ↥(HCPolySupport.HilbertVectorL2 U)) (FV : ↥(HCPolySupport.HilbertVectorL2 V)) (GU : ↥(HCPolySupport.HilbertVectorL2 U)) (GV : ↥(HCPolySupport.HilbertVectorL2 V)) (hF : ↑↑FU =ᵐ[HCPolySupport.volumeMeasureOn U] V.indicator fun (x : HCPolySupport.Vec d) => ↑↑FV x) (hG : ↑↑GV =ᵐ[HCPolySupport.volumeMeasureOn V] ↑↑GU) :
coefficientPairing a U FU GU = coefficientPairing a V FV GV
source
theorem DivergenceFormProcess.Form.scalar_inner_restriction_le {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (hVU : V ⊆ U) (fU : ↥(HCPolySupport.ScalarL2 U)) (fV : ↥(HCPolySupport.ScalarL2 V)) (φU : ↥(HCPolySupport.ScalarL2 U)) (φV : ↥(HCPolySupport.ScalarL2 V)) (hfV : ↑↑fV =ᵐ[HCPolySupport.volumeMeasureOn V] ↑↑fU) (hφV : ↑↑φV =ᵐ[HCPolySupport.volumeMeasureOn V] ↑↑φU) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑fU x) (hφ : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑φU x) :
inner ℝ fV φV ≤ inner ℝ fU φU
source
noncomputable def DivergenceFormProcess.Form.restrictScalarL2ToPart {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) (f : ↥(HCPolySupport.ScalarL2 U)) :
↥(HCPolySupport.ScalarL2 V)

Restriction of scalar L² data to a measurable part domain.

Equations
Instances For
    source
    theorem DivergenceFormProcess.Form.restrictScalarL2ToPart_coeFn {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (hV : MeasurableSet V) (hU : MeasurableSet U) (hVU : V ⊆ U) (f : ↥(HCPolySupport.ScalarL2 U)) :
    ↑↑(restrictScalarL2ToPart hU f) =ᵐ[HCPolySupport.volumeMeasureOn V] ↑↑f

    Almost-everywhere characterization of scalar L² restriction between nested measurable domains.

    source
    noncomputable def DivergenceFormProcess.Form.ZeroTraceSobolev.extendByZeroToPartSuperset {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (hU : IsOpen U) (hVU : V ⊆ U) (u : ZeroTraceSobolev V) :
    ZeroTraceSobolev U

    Canonical zero extension of a zero-trace Sobolev element from a bounded open convex domain to an open superset.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem DivergenceFormProcess.Form.ZeroTraceSobolev.extendByZeroToPartSuperset_toL2 {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (hU : IsOpen U) (hVU : V ⊆ U) (u : ZeroTraceSobolev V) :
      ↑↑(toL2 (extendByZeroToPartSuperset hV hU hVU u)) =ᵐ[HCPolySupport.volumeMeasureOn U] V.indicator fun (x : HCPolySupport.Vec d) => ↑↑(toL2 u) x

      The value of the canonical zero extension is the indicator extension.

      source
      theorem DivergenceFormProcess.Form.ZeroTraceSobolev.extendByZeroToPartSuperset_gradient {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (hU : IsOpen U) (hVU : V ⊆ U) (u : ZeroTraceSobolev V) :
      ↑↑(gradient (extendByZeroToPartSuperset hV hU hVU u)) =ᵐ[HCPolySupport.volumeMeasureOn U] V.indicator fun (x : HCPolySupport.Vec d) => ↑↑(gradient u) x

      The weak gradient of the canonical zero extension is the indicator extension of the original weak gradient.