Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.CorrectorGlobalRepresentative

High-contrast homogenization: Provider.Regularity.CorrectorGlobalRepresentative #

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

Global representatives of projective local correctors #

Compatible local value and gradient L² classes are glued along the disjoint shells of the centered-cube exhaustion. The resulting raw fields are strongly measurable and agree almost everywhere with every stored local component.

source
def HCPolySupport.HighContrast.localGradientShell (d a✝ : ℕ) :
Set (Vec d)

The disjoint shell added at the nth stage of the centered-cube exhaustion.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.measurableSet_localGradientShell (d n : ℕ) :
    MeasurableSet (localGradientShell d n)

    Every exhaustion shell is measurable.

    source
    theorem HCPolySupport.HighContrast.localGradientShell_subset_cube (d n : ℕ) :
    localGradientShell d n ⊆ localGradientCube d n

    The nth shell lies in the nth exhaustion cube.

    source
    theorem HCPolySupport.HighContrast.localGradientCube_union_shell (d n : ℕ) :
    localGradientCube d n ∪ localGradientShell d (n + 1) = localGradientCube d (n + 1)

    Adding the successor shell to an exhaustion cube gives the next cube.

    source
    theorem HCPolySupport.HighContrast.pairwise_disjoint_localGradientShell (d : ℕ) :
    Pairwise fun (i j : ℕ) => Disjoint (localGradientShell d i) (localGradientShell d j)

    Distinct exhaustion shells are disjoint.

    source
    theorem HCPolySupport.HighContrast.iUnion_localGradientShell (d : ℕ) :
    ⋃ (n : ℕ), localGradientShell d n = Set.univ

    The shells exhaust the whole Euclidean space.

    source
    theorem HCPolySupport.HighContrast.localGradientShell_compat {d : ℕ} {E : Type u_1} (f : (n : ℕ) → ↑(localGradientShell d n) → E) (i j : ℕ) (x : Vec d) (hxi : x ∈ localGradientShell d i) (hxj : x ∈ localGradientShell d j) :
    f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
    source
    noncomputable def HCPolySupport.HighContrast.localGradientShellLift {d : ℕ} {E : Type u_1} (f : (n : ℕ) → ↑(localGradientShell d n) → E) :
    Vec d → E

    Glue arbitrary shellwise fields into a global field.

    Equations
    Instances For
      source
      theorem HCPolySupport.HighContrast.localGradientShellLift_of_mem {d : ℕ} {E : Type u_1} (f : (n : ℕ) → ↑(localGradientShell d n) → E) (n : ℕ) {x : Vec d} (hx : x ∈ localGradientShell d n) :
      localGradientShellLift f x = f n ⟨x, hx⟩

      The shell lift reads the supplied field on each shell.

      source
      theorem HCPolySupport.HighContrast.measurable_localGradientShellLift {d : ℕ} {E : Type u_1} [MeasurableSpace E] (f : (n : ℕ) → ↑(localGradientShell d n) → E) (hf : ∀ (n : ℕ), Measurable (f n)) :
      Measurable (localGradientShellLift f)

      Measurable shellwise fields have a measurable shell lift.

      source
      noncomputable def HCPolySupport.HighContrast.localValueStrongRepresentative {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) :
      Vec d → ℝ

      A strongly measurable representative of the local H¹ value component on exhaustion cube n.

      Equations
      Instances For
        source
        noncomputable def HCPolySupport.HighContrast.localGradientVectorComponent {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) :
        ↥(VectorL2 (localGradientCube d n))

        The local gradient component on exhaustion cube n, expressed in the algebraic vector L² space.

        Equations
        Instances For
          source
          noncomputable def HCPolySupport.HighContrast.localGradientStrongRepresentative {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) :
          Vec d → Vec d

          A strongly measurable representative of the vector L² gradient on exhaustion cube n.

          Equations
          Instances For
            source
            noncomputable def HCPolySupport.HighContrast.NormalizedLocalH1Carrier.globalValueRepresentative {d : ℕ} (z : NormalizedLocalH1Carrier d) :
            Vec d → ℝ

            A global scalar representative of the projective local value classes.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def HCPolySupport.HighContrast.NormalizedLocalH1Carrier.globalGradientRepresentative {d : ℕ} (z : NormalizedLocalH1Carrier d) :
              Vec d → Vec d

              A global Euclidean representative of the projective local gradient classes.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.stronglyMeasurable_globalValueRepresentative {d : ℕ} (z : NormalizedLocalH1Carrier d) :
                MeasureTheory.StronglyMeasurable z.globalValueRepresentative

                The global value representative is strongly measurable.

                source
                theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.stronglyMeasurable_globalGradientRepresentative {d : ℕ} (z : NormalizedLocalH1Carrier d) :
                MeasureTheory.StronglyMeasurable z.globalGradientRepresentative

                The global gradient representative is strongly measurable.

                source
                theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.globalValueRepresentative_ae_eq_component {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) :
                z.globalValueRepresentative =ᵐ[volumeMeasureOn (localGradientCube d n)] ↑↑(z.valueComponent n)

                On every exhaustion cube, the global scalar representative agrees almost everywhere with the stored scalar L² component.

                source
                theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.globalGradientRepresentative_ae_eq_component {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) :
                z.globalGradientRepresentative =ᵐ[volumeMeasureOn (localGradientCube d n)] ↑↑(hilbertVectorL2ToVectorL2 (z.gradientComponent n))

                On every exhaustion cube, the global Euclidean gradient representative agrees almost everywhere with the vector form of the stored gradient component.

                source
                theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.memLp_globalValueRepresentative {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) :
                MeasureTheory.MemLp z.globalValueRepresentative 2 (volumeMeasureOn (localGradientCube d n))

                The global scalar representative is square-integrable on every exhaustion cube.

                source
                theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.memLp_globalGradientRepresentative {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) :
                MeasureTheory.MemLp z.globalGradientRepresentative 2 (volumeMeasureOn (localGradientCube d n))

                The global gradient representative is square-integrable on every exhaustion cube.

                source
                theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.globalValueRepresentative_ae_eq_localH1Function {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) :
                z.globalValueRepresentative =ᵐ[volumeMeasureOn (localGradientCube d n)] (z.localH1Function n).toFun

                On each exhaustion cube, the global scalar representative agrees almost everywhere with the canonical recovered local H¹ function.

                source
                theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.globalGradientRepresentative_ae_eq_localH1Gradient {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) :
                z.globalGradientRepresentative =ᵐ[volumeMeasureOn (localGradientCube d n)] (z.localH1Function n).grad

                On each exhaustion cube, the global Euclidean gradient representative agrees almost everywhere with the weak gradient of the canonical recovered local H¹ function.