Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.WeakNormSquareIntegrability

Coarse-graining support: #

Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.WeakNormSquareIntegrability

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Special-vector weak-norm square integrability #

This proof-internal file discharges the finite-RHS side conditions inherited from the first Section 5.3 lemma, in the special-vector regime used by the coarse-fluctuation lemma.

source
@[irreducible]
noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.Internal.specialGradientWeakNormSquare {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) (a : RegCoeffField d) :
ℝ

The squared gradient weak norm for the special response vectors on the scale-m origin cube, with exponent sLower + 2 * β and centered slope p0_e.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[irreducible]
    noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.Internal.specialFluxWeakNormSquare {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) (a : RegCoeffField d) :
    ℝ

    The squared flux weak norm for the special response vectors on the scale-m origin cube, with exponent sUpper + 2 * β and centered flux q0_e.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[irreducible]
      noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.Internal.specialPairedWeakNormSquare {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) (a : RegCoeffField d) :
      ℝ

      The special-vector paired weak-norm square: the gradient square weighted by sigmaHatAtScale plus the flux square weighted by its inverse.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[irreducible]
        noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.Internal.specialWeakNormComponentSquareSum {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (k m : ℕ) (e : Vec d) (a : RegCoeffField d) :
        ℝ

        The special-vector weak-norm square budget combining average, mismatch, low-scale, and constant-tail squares, with maximizer weights and an overall factor 16.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.integrable_paired_specialWeakNormSquares_from_weakNormMaximizer {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {k m : ℕ} (hkm : k < m) (e : Vec d) (he : vecNormSq e = 1) :
          MeasureTheory.Integrable (Internal.specialPairedWeakNormSquare hP hStruct hP4 m e) P

          The paired special-vector weak-norm square is integrable. This is the non-circular version: the left side is integrated by domination from the second Section 5.3 weak-norm maximizer estimate and the already proved component-square integrability facts.

          source
          theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.integrable_specialGradientWeakNormSquare_from_weakNormMaximizer {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {k m : ℕ} (hkm : k < m) (e : Vec d) (he : vecNormSq e = 1) :
          MeasureTheory.Integrable (Internal.specialGradientWeakNormSquare hP hStruct hP4 m e) P

          Special-vector gradient weak-norm square integrability from the second Section 5.3 weak-norm maximizer lemma.

          source
          theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.integrable_specialFluxWeakNormSquare_from_weakNormMaximizer {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {k m : ℕ} (hkm : k < m) (e : Vec d) (he : vecNormSq e = 1) :
          MeasureTheory.Integrable (Internal.specialFluxWeakNormSquare hP hStruct hP4 m e) P

          Special-vector flux weak-norm square integrability from the second Section 5.3 weak-norm maximizer lemma.