Documentation

LeanPool.HighContrastHomogenization.Entry.Response.Core.LoadMeanIdentity

High-contrast homogenization: Entry.Response.Core.LoadMeanIdentity #

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

The response load and mean identity #

This file proves the mean identity and the load/mean bounds e.response.load.and.mean of the decomposition of adapted_response_core: it shows the block mean respM0 is symmetric, positive definite and self-inverse under multiplication, expands the associated quadratic form under block scaling and under a Loewner bound, and combines these into the response load-and-mean estimate response_load_and_mean. The supporting matrix identities — the block-matrix-vector product under scaling, the transpose of the full block matrix, and the quadratic-form symmetry and expansion lemmas — are proved along the way.

R1 decomposition, part 3: the mean identity and the load/mean bounds #

The two parts of the decomposition of R1 adapted_response_core: the mean identity and the load/mean bounds.

The mean identity #

The load/mean bounds #

Helpers for the load/mean bounds #

The block-algebra lemmas the proof of response_load_and_mean rests on. They are private and local to this file; four of them (respM0_qform_eq_sum_vecDot, respM0_isSymm_of_metric_posDef, respM0_blockPosDef_of_metric_posDef, blockSqrt_qform) repeat the public declarations respM0_qform_split_canonicalMetric and blockSqrt_qform_blockVecDot of HCPoly/Entry/Response/Core/SourceLoadBound.lean and respM0_isSymm_of_canonicalMetric_posDef and respM0_blockPosDef_of_canonicalMetric_posDef of HCPoly/Entry/Response/Core/AnnealedMeanDrift.lean.

M_0 and the swap #

source
noncomputable def HCPolySupport.HighContrast.Multiscale.respM0inv {d : ℕ} (F : BlockMat d) :
BlockMat d

M_0^{-1} = diag(m^{-1}, m).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.Multiscale.respM0_full_posDef {d : ℕ} {F : BlockMat d} (hm : Matrix.PosDef (explicitCanonicalMetric F)) :
    Matrix.PosDef (toFullBlockMat (respM0 F))

    The operator inequality Ê M_0^{-1} Ê ≤ λ Ê #

    The two bounds for one sign #

    The load/mean bounds #

    source
    theorem HCPolySupport.HighContrast.Multiscale.response_load_and_mean (d : ℕ) (_hd : 2 ≤ d) (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (_hS : S.Selects d γ) (Cc Ce : ℝ) (_hCc : 0 < Cc) (_hCe : 0 < Ce) :
    ∃ (C : ℝ), 0 < C ∧ ∀ (ε σ : ℝ), ε ∈ Set.Ioc 0 S.eps0 → σ ∈ Set.Ioc 0 ε → ∀ (Cglob Cprof Csrc Bresp : ℝ) (H : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (Kg : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ), RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ Kg Src B jStar F s t → RespCalibrated Cc P jStar F s t → ∀ (e : Vec d), vecDot e e = 1 → RespEnergyDefect Ce P jStar F s t e → RespLoadMean C P jStar F s t e

    The load/mean bounds e.response.load.and.mean: |M_0^{1/2}x^±|^2 <= C kappa_s^{1/2} and |M_0^{1/2}Y^±|^2 <= C kappa_s.

    Route, as printed. Write Q_A(X) = X · A X, x = x^±, Ê = Ê_t^±, w = Ê x.

    • M_0^{1/2} is a square root on quadratic forms (blockSqrt_qform), so both printed left-hand sides are Q_{M_0}(x) and Q_{M_0}(Y).
    • The load bound is the lower calibrated block alone: C_c^{-1}M_0 <= Ê gives Q_{M_0}(x) <= C_c Q_Ê(x) = C_c (L^±)^2, and (L^±)^2 = 2E[J_t^±] + 2 <= 2C_e kappa_s^{1/2} + 2 is the energy-defect bound (RespEnergyDefect).
    • For the mean bound, Y = (I + R Ê)x is blockResponseMean, i.e. respYMinus/respYPlus by definition, so Q_{M_0}(Y) <= 2 Q_{M_0}(x) + 2 Q_{M_0}(R w). Since R M_0 R = M_0^{-1} (swap_qform: both sides are p·m p + q·m^{-1}q with the two components exchanged), Q_{M_0}(R w) = w · M_0^{-1} w, and the operator inequality Ê M_0^{-1} Ê <= C kappa_t^{1/2} Ê of the printed proof is responseLoadMean_core: with lam = C_c kappa_t^{1/2} from the upper calibrated block, 0 <= (x - lam^{-1}M_0^{-1}w)·Ê (x - lam^{-1}M_0^{-1}w) expands to w·M_0^{-1}w <= lam Q_Ê(x). No square root and no Cauchy-Schwarz is needed.
    • The two are combined with 1 <= kappa_t <= kappa_s (response_imbalance_comparison): Q_{M_0}(Y) <= (2C_c + 2C_c kappa_t^{1/2})(2(C_e+1)kappa_s^{1/2}) <= (4C_c kappa_s^{1/2})(2(C_e+1)kappa_s^{1/2}) = 8C_c(C_e+1)kappa_s.

    The constant is C = 8 C_c (C_e + 1).

    The statement carries the two premises _hε : ε ∈ Set.Ioc 0 S.eps0 and _hσ : σ ∈ Set.Ioc 0 ε, as do the other results of the decomposition. They are needed for the same reason: without them S.one_le_B0 is unavailable, hence 1 ≤ B, hence j_* < s (jStar_lt_s_of_raw), hence E_t ≤ E_s and the comparison kappa_t ≤ kappa_s are unavailable -- and the printed mean bound is C kappa_s, not C kappa_t^{1/2} kappa_s^{1/2}, so the comparison is genuinely needed. R1 carries both premises, and the application passes hε hσε, which are in scope there.