Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.RuledWhitneyRowCauchySchwarz

High-contrast homogenization: Provider.PolynomialHomogenization.RuledWhitneyRowCauchySchwarz #

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

source
noncomputable def HCPolySupport.HighContrast.rawWhitneyRowEnergy {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (X : system.CellIndex → ENNReal) :
ENNReal

The unnormalized volume-weighted square row associated with a nonnegative cell quantity.

Equations
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.normalizedWhitneyRowEnergy {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (X : system.CellIndex → ENNReal) :
    ENNReal

    The volume-normalized square row associated with a nonnegative cell quantity.

    Equations
    Instances For
      source
      theorem HCPolySupport.HighContrast.tsum_rpow_half_mul_rpow_half_le {ι : Type u_1} [Countable ι] (A B : ι → ENNReal) :
      ∑' (i : ι), A i ^ (1 / 2) * B i ^ (1 / 2) ≤ (∑' (i : ι), A i) ^ (1 / 2) * (∑' (i : ι), B i) ^ (1 / 2)

      Countable Cauchy--Schwarz for extended nonnegative rows.

      source
      theorem HCPolySupport.HighContrast.whitneyCellIntegrals_le_row_cauchySchwarz {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) {f : Vec d → ℝ} (N P : system.CellIndex → ENNReal) (hcell : ∀ (i : system.CellIndex), ENNReal.ofReal |volumeAverage (system.cell i) f| ≤ N i ^ (1 / 2) * P i ^ (1 / 2)) :
      ∑' (i : system.CellIndex), ENNReal.ofReal |∫ (x : Vec d) in system.cell i, f x| ≤ rawWhitneyRowEnergy system N ^ (1 / 2) * rawWhitneyRowEnergy system P ^ (1 / 2)

      If every normalized cell pairing is bounded by the product of a negative and positive cell size, then the sum of raw cell pairings is bounded by the product of the two volume-weighted square rows.

      source
      theorem HCPolySupport.HighContrast.ofReal_abs_volumeAverage_le_whitneyRow_cauchySchwarz {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hd : 1 ≤ d) (hU : IsOpenBoundedConvexDomain U) {f : Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f U MeasureTheory.volume) (N P : system.CellIndex → ENNReal) (hcell : ∀ (i : system.CellIndex), ENNReal.ofReal |volumeAverage (system.cell i) f| ≤ N i ^ (1 / 2) * P i ^ (1 / 2)) :
      ENNReal.ofReal |volumeAverage U f| ≤ ENNReal.ofReal (MeasureTheory.volume U).toReal⁻¹ * (rawWhitneyRowEnergy system N ^ (1 / 2) * rawWhitneyRowEnergy system P ^ (1 / 2))

      The domain pairing is controlled by the two ruled Whitney square rows once the local dual estimate is known on every cell.