Documentation

LeanPool.HighContrastHomogenization.Provider.Response.WeakNorm

High-contrast homogenization: Provider.Response.WeakNorm #

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

The adapted concrete weak norm #

The weak-norm estimate for the optimizer state measures the doubled block state of a response maximizer in the concrete scale-average seminorm,

[F]_{B^{-s}_{2,1}(U_t)} = Σ_{k = -∞}^{t} 3^{sk}
    ( avsum_{z ∈ 𝒡_{k,t}^q} |(F)_{U_k(z)}|^2 )^{1/2},

on the adapted cube U_t = qβ–‘_t subdivided into the aligned cells U_k(z) = z + qβ–‘_k, z ∈ 𝒡_{k,t}^q = 3^k𝕃_q ∩ U_t. This is the concrete seminorm of [Armstrong–Kuusi, (2.130)], not the negative Besov dual norm: no duality, no projection, and no cutoff enters, and the only structure the cells carry is their exact partition of the parent β€” its count and its equal volumes.

This module carries the definitions and their defining equations; the way the cell average meets the metric root and the centering is the companion module.

The k-sum runs to -∞ and is not asserted convergent, so the seminorm is valued in ℝβ‰₯0∞, where the sum of a family of nonnegative terms is always defined and monotone; the lemma is asserted "valid when its right side is infinite". Each summand is a genuine nonnegative real β€” the inner average is a normalized sum of squared Euclidean lengths β€” so no truncation happens below the level of the k-sum, and the real value is recovered on the summable branch.

The aligned index set #

source
noncomputable def HCPolySupport.HighContrast.Response.alignedIndex {d : β„•} (q : Mat d) (j p : β„€) :
Finset (Fin d β†’ β„€)

The aligned index 𝒡_{j,p}^q = 3^j𝕃_q ∩ β‹„_p^q of the adapted cells, carried by the lattice labels of its centres: the labels w for which the aligned centre 3^jqw lies in the parent cell. The set of such labels is finite exactly on the printed range j ≀ p of a positive grid, and there the definition returns it.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.Response.coe_alignedIndex {d : β„•} {q : Mat d} (hq : Matrix.PosDef q) {j p : β„€} (hjp : j ≀ p) :
    ↑(alignedIndex q j p) = {w : Fin d β†’ β„€ | adaptedCellCenter q j w ∈ adaptedCell q p}

    The defining equation of the aligned index: on the printed range its elements are exactly the labels of the aligned centres inside the parent cell.

    source
    theorem HCPolySupport.HighContrast.Response.mem_alignedIndex_iff {d : β„•} {q : Mat d} (hq : Matrix.PosDef q) {j p : β„€} (hjp : j ≀ p) {w : Fin d β†’ β„€} :
    w ∈ alignedIndex q j p ↔ adaptedCellCenter q j w ∈ adaptedCell q p

    Membership in the aligned index.

    source
    theorem HCPolySupport.HighContrast.Response.card_alignedIndex {d : β„•} {q : Mat d} (hq : Matrix.PosDef q) {j p : β„€} (hjp : j ≀ p) :
    (alignedIndex q j p).card = 3 ^ (d * (p - j).toNat)

    #𝒡_{j,p}^q = 3^{d(p-j)}, the count of the aligned children of a cell.

    source
    theorem HCPolySupport.HighContrast.Response.alignedIndex_nonempty {d : β„•} {q : Mat d} (hq : Matrix.PosDef q) {j p : β„€} (hjp : j ≀ p) :
    (alignedIndex q j p).Nonempty

    The aligned index is nonempty: it has 3^{d(p-j)} elements.

    source
    theorem HCPolySupport.HighContrast.Response.adaptedCellAt_subset_of_mem_alignedIndex {d : β„•} {q : Mat d} (hq : Matrix.PosDef q) {j p : β„€} (hjp : j ≀ p) {w : Fin d β†’ β„€} (hw : w ∈ alignedIndex q j p) :
    adaptedCellAt q j w βŠ† adaptedCell q p

    The aligned cells sit inside the parent cell: the containment U_k(z) βŠ† U_t of the adapted cells.

    The normalized cell average #

    source
    noncomputable def HCPolySupport.HighContrast.Response.avsum {ΞΉ : Type u_1} (Z : Finset ΞΉ) (f : ΞΉ β†’ ℝ) :
    ℝ

    The printed normalized average avsum_{z ∈ 𝒡} f(z) = 3^{-d(t-k)}Ξ£_z f(z) over the aligned children of a cell, written with the reciprocal cardinality so that no count has to be substituted before it is used.

    Equations
    Instances For
      source
      theorem HCPolySupport.HighContrast.Response.avsum_eq {ΞΉ : Type u_1} (Z : Finset ΞΉ) (f : ΞΉ β†’ ℝ) :
      avsum Z f = (↑Z.card)⁻¹ * βˆ‘ z ∈ Z, f z

      The defining equation of the normalized average.

      source
      theorem HCPolySupport.HighContrast.Response.avsum_nonneg {ΞΉ : Type u_1} {Z : Finset ΞΉ} {f : ΞΉ β†’ ℝ} (hf : βˆ€ z ∈ Z, 0 ≀ f z) :
      0 ≀ avsum Z f

      A normalized average of nonnegative terms is nonnegative.

      source
      theorem HCPolySupport.HighContrast.Response.avsum_const {ΞΉ : Type u_1} {Z : Finset ΞΉ} (hZ : Z.Nonempty) (c : ℝ) :
      (avsum Z fun (x : ΞΉ) => c) = c

      The normalized average of a constant is that constant.

      source
      theorem HCPolySupport.HighContrast.Response.avsum_le_avsum {ΞΉ : Type u_1} {Z : Finset ΞΉ} {f g : ΞΉ β†’ ℝ} (h : βˆ€ z ∈ Z, f z ≀ g z) :
      avsum Z f ≀ avsum Z g

      The normalized average is monotone.

      source
      theorem HCPolySupport.HighContrast.Response.avsum_le_of_forall_le {ΞΉ : Type u_1} {Z : Finset ΞΉ} {f : ΞΉ β†’ ℝ} {c : ℝ} (hZ : Z.Nonempty) (h : βˆ€ z ∈ Z, f z ≀ c) :
      avsum Z f ≀ c

      A normalized average is at most a uniform upper bound of its terms.

      source
      theorem HCPolySupport.HighContrast.Response.avsum_add {ΞΉ : Type u_1} (Z : Finset ΞΉ) (f g : ΞΉ β†’ ℝ) :
      (avsum Z fun (z : ΞΉ) => f z + g z) = avsum Z f + avsum Z g

      The normalized average is additive.

      source
      theorem HCPolySupport.HighContrast.Response.avsum_const_mul {ΞΉ : Type u_1} (Z : Finset ΞΉ) (c : ℝ) (f : ΞΉ β†’ ℝ) :
      (avsum Z fun (z : ΞΉ) => c * f z) = c * avsum Z f

      A constant factors out of the normalized average.

      The cell average of a doubled field #

      source
      noncomputable def HCPolySupport.HighContrast.Response.blockCellAverage {d : β„•} (U : Set (Vec d)) (F : Vec d β†’ BlockVec d) :
      BlockVec d

      The cell average (F)_U of an ℝ^{2d}-valued field, taken slotwise: this is the quantity the scale-average seminorm evaluates on every aligned cell.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem HCPolySupport.HighContrast.Response.blockCellAverage_fst {d : β„•} (U : Set (Vec d)) (F : Vec d β†’ BlockVec d) :
        (blockCellAverage U F).1 = volumeAverageVec U fun (x : Vec d) => (F x).1

        The first slot of the cell average.

        source
        @[simp]
        theorem HCPolySupport.HighContrast.Response.blockCellAverage_snd {d : β„•} (U : Set (Vec d)) (F : Vec d β†’ BlockVec d) :
        (blockCellAverage U F).2 = volumeAverageVec U fun (x : Vec d) => (F x).2

        The second slot of the cell average.

        source
        theorem HCPolySupport.HighContrast.Response.blockCellAverage_gradFlux {d : β„•} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (v : Book.Ch02.Solution U a) :
        (blockCellAverage U.carrier fun (x : Vec d) => (v.toH1.grad x, matVecMul (a.toCoeffField x) (v.toH1.grad x))) = (Book.Ch02.averageGradient U a v, Book.Ch02.averageFlux U a v)

        The cell average of the doubled optimizer state: for X(V) = (βˆ‡v, aβˆ‡v) the slotwise average is the pair of averages the variational average identity is written on.

        The metric quadratic form #

        source
        noncomputable def HCPolySupport.HighContrast.Response.metricBlockNormSq {d : β„•} (m : Mat d) (v : BlockVec d) :
        ℝ

        The squared metric length |M_0^{1/2}v|^2 = vΒ·M_0v of the diagonal metric M_0 = diag(m_0, m_0^{-1}), read as a quadratic form. This is the reading of its self-duality that the weak-norm estimate uses; it needs no matrix root.

        Equations
        Instances For
          source
          theorem HCPolySupport.HighContrast.Response.metricBlockNormSq_eq {d : β„•} (m : Mat d) (v : BlockVec d) :
          metricBlockNormSq m v = vecDot v.1 (matVecMul m v.1) + vecDot v.2 (matVecMul m⁻¹ v.2)

          The defining equation of the metric quadratic form, slot by slot.

          The seminorm #

          source
          noncomputable def HCPolySupport.HighContrast.Response.blockAvsumL2 {d : β„•} {ΞΉ : Type u_1} (Z : Finset ΞΉ) (g : ΞΉ β†’ BlockVec d) :
          ℝ

          The inner factor (avsum_{z ∈ 𝒡}|g(z)|^2)^{1/2} of the scale-average seminorm: the normalized β„“^2 length of a family of ℝ^{2d} vectors indexed by the aligned centres of one scale.

          Equations
          Instances For
            source
            theorem HCPolySupport.HighContrast.Response.blockAvsumL2_eq {d : β„•} {ΞΉ : Type u_1} (Z : Finset ΞΉ) (g : ΞΉ β†’ BlockVec d) :
            blockAvsumL2 Z g = √(avsum Z fun (z : ι) => blockVecDot (g z) (g z))

            The defining equation of the normalized β„“^2 length.

            source
            theorem HCPolySupport.HighContrast.Response.blockVecDot_self_nonneg {d : β„•} (v : BlockVec d) :
            0 ≀ blockVecDot v v

            The squared Euclidean length of a doubled vector is nonnegative.

            source
            theorem HCPolySupport.HighContrast.Response.blockAvsumL2_nonneg {d : β„•} {ΞΉ : Type u_1} (Z : Finset ΞΉ) (g : ΞΉ β†’ BlockVec d) :
            0 ≀ blockAvsumL2 Z g

            The normalized β„“^2 length is nonnegative.

            source
            noncomputable def HCPolySupport.HighContrast.Response.adaptedWeakScaleTerm {d : β„•} (q : Mat d) (t : β„€) (s : ℝ) (F : Vec d β†’ BlockVec d) (j : β„•) :
            ℝ

            One summand 3^{sk}(avsum_z |(F)_{U_k(z)}|^2)^{1/2} of the scale-average seminorm, at the scale k = t - j.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem HCPolySupport.HighContrast.Response.adaptedWeakScaleTerm_eq {d : β„•} (q : Mat d) (t : β„€) (s : ℝ) (F : Vec d β†’ BlockVec d) (j : β„•) :
              adaptedWeakScaleTerm q t s F j = 3 ^ (s * (↑t - ↑j)) * blockAvsumL2 (alignedIndex q (t - ↑j) t) fun (z : Fin d β†’ β„€) => blockCellAverage (adaptedCellAt q (t - ↑j) z) F

              The defining equation of one scale summand.

              source
              noncomputable def HCPolySupport.HighContrast.Response.adaptedWeakSeminorm {d : β„•} (q : Mat d) (t : β„€) (s : ℝ) (F : Vec d β†’ BlockVec d) :
              ENNReal

              The concrete scale-average seminorm [F]_{B^{-s}_{2,1}(U_t)} on the adapted cube U_t = qβ–‘_t with its aligned subdivision. The printed sum runs over all scales k ≀ t, reindexed here by k = t - j, j ∈ β„•; it is carried in ℝβ‰₯0∞, where the sum of a family of nonnegative terms is always defined, so that the estimate is asserted also when its right side is infinite.

              Equations
              Instances For
                source
                theorem HCPolySupport.HighContrast.Response.adaptedWeakSeminorm_eq {d : β„•} (q : Mat d) (t : β„€) (s : ℝ) (F : Vec d β†’ BlockVec d) :
                adaptedWeakSeminorm q t s F = βˆ‘' (j : β„•), ENNReal.ofReal (adaptedWeakScaleTerm q t s F j)

                The defining equation of the seminorm: the sum over all scales k ≀ t of the printed summands.