High-contrast homogenization: Provider.Response.ProfileCarriers

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

Terminal profile carriers

This file names the centered, below-start, and complete terminal maxima from e.scale.selection.fluctuation.history and from the below-start source maximum at the response scale. It also records the finite window coefficients, bad-event majorant, and response-energy load used in the passage from the terminal profiles to the response bounds in p.response.transfer.

The two suprema and their moments take values in ℝ≥0∞, so divergence is represented by the top element. The window coefficients remain finite sums; no sign is assumed for 1 / 2 - rhoMax.

Centered and below-start maxima

noncomputable def HCPolySupport.HighContrast.Response.profileCenteredMaximum {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (rhoMax : ℝ) (q : Mat d) (jStar t : ℤ) (a : CoeffSpace d) : ENNReal

The centered terminal maximum Z_t.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Response.profileCenteredMaximum_eq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (rhoMax : ℝ) (q : Mat d) (jStar t : ℤ) (a : CoeffSpace d) : profileCenteredMaximum P rhoMax q jStar t a = ⨆ (k : ℤ), ⨆ (_ : jStar ≤ k), ⨆ (_ : k ≤ t), ⨆ (w : Fin d → ℤ), ⨆ (_ : adaptedCellCenter q k w ∈ adaptedCell q t), ENNReal.ofReal (3 ^ (-rhoMax * (↑t - ↑k)) * blockSize (blockSub (adaptedResponse q k w a) (adaptedMean P q k)) (adaptedMean P q t))

The defining equation for Z_t.

noncomputable def HCPolySupport.HighContrast.Response.profileSourceMaximum {d : ℕ} (rhoMax : ℝ) (q : Mat d) (jStar t : ℤ) (F : BlockMat d) (a : CoeffSpace d) : ENNReal

The exact below-start maximum B_src(t).

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Response.profileSourceMaximum_eq {d : ℕ} (rhoMax : ℝ) (q : Mat d) (jStar t : ℤ) (F : BlockMat d) (a : CoeffSpace d) : profileSourceMaximum rhoMax q jStar t F a = belowStartSup rhoMax q jStar t (fun (k : ℤ) => containedCenters q k t) F a

The defining equation for B_src(t).

noncomputable def HCPolySupport.HighContrast.Response.profileSourceMoment {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (Q rhoMax : ℝ) (q : Mat d) (jStar t : ℤ) (F : BlockMat d) : ENNReal

The source moment b_Q(t).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.Response.profileTotalMaximum {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (rhoMax : ℝ) (q : Mat d) (jStar t : ℤ) (F : BlockMat d) (a : CoeffSpace d) : ENNReal

The complete terminal maximum W_t = Z_t + B_src(t).

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Response.profileTotalMaximum_eq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (rhoMax : ℝ) (q : Mat d) (jStar t : ℤ) (F : BlockMat d) (a : CoeffSpace d) : profileTotalMaximum P rhoMax q jStar t F a = profileCenteredMaximum P rhoMax q jStar t a + profileSourceMaximum rhoMax q jStar t F a

The defining equation for W_t.

noncomputable def HCPolySupport.HighContrast.Response.profileTotalHistory {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (Q rhoMax : ℝ) (q : Mat d) (jStar t : ℤ) (F : BlockMat d) : ENNReal

The complete terminal history ᵍ_t^tot = E[W_t^Q].

Equations

• One or more equations did not get rendered due to their size.

Scalar coefficients

noncomputable def HCPolySupport.HighContrast.Response.profileBadMajorant (Q h beta : ℝ) : ℝ

The two-branch correlated bad-event majorant 𝔅_Q(h,β).

Equations

• HCPolySupport.HighContrast.Response.profileBadMajorant Q h beta = if beta < 1 then (h ^ Q⁻¹ + beta) * (1 - beta) ^ (1 - Q / 2) * h ^ (1 / 2 - Q⁻¹) else h ^ Q⁻¹ + beta

theorem HCPolySupport.HighContrast.Response.profileBadMajorant_of_lt_one {Q h beta : ℝ} (hbeta : beta < 1) : profileBadMajorant Q h beta = (h ^ Q⁻¹ + beta) * (1 - beta) ^ (1 - Q / 2) * h ^ (1 / 2 - Q⁻¹)

The defining equation for the small-drift branch of 𝔅_Q.

theorem HCPolySupport.HighContrast.Response.profileBadMajorant_of_one_le {Q h beta : ℝ} (hbeta : 1 ≤ beta) : profileBadMajorant Q h beta = h ^ Q⁻¹ + beta

The defining equation for the large-drift branch of 𝔅_Q.

noncomputable def HCPolySupport.HighContrast.Response.profileBadMajorantAt (Q h beta lev : ℝ) : ℝ

The two-branch bad-event majorant at a released split level. The fixed-level profileBadMajorant is this at lev = 1: the guard beta < 1 becomes beta < lev, and the drift denominator 1 - beta becomes lev - beta.

Equations

• HCPolySupport.HighContrast.Response.profileBadMajorantAt Q h beta lev = if beta < lev then (h ^ Q⁻¹ + beta) * (lev - beta) ^ (1 - Q / 2) * h ^ (1 / 2 - Q⁻¹) else h ^ Q⁻¹ + beta

theorem HCPolySupport.HighContrast.Response.profileBadMajorantAt_of_lt {Q h beta lev : ℝ} (hbeta : beta < lev) : profileBadMajorantAt Q h beta lev = (h ^ Q⁻¹ + beta) * (lev - beta) ^ (1 - Q / 2) * h ^ (1 / 2 - Q⁻¹)

The small-drift branch.

theorem HCPolySupport.HighContrast.Response.profileBadMajorantAt_of_ge {Q h beta lev : ℝ} (hbeta : lev ≤ beta) : profileBadMajorantAt Q h beta lev = h ^ Q⁻¹ + beta

The large-drift branch.

theorem HCPolySupport.HighContrast.Response.profileBadMajorantAt_nonneg {Q h beta lev : ℝ} (hh : 0 ≤ h) (hbeta : 0 ≤ beta) : 0 ≤ profileBadMajorantAt Q h beta lev

noncomputable def HCPolySupport.HighContrast.Response.centeredWindowCoefficient (H : ℕ) (rhoMax : ℝ) : ℝ

The finite centered-window coefficient S_cen.

Equations

• HCPolySupport.HighContrast.Response.centeredWindowCoefficient H rhoMax = 2 * ∑ r ∈ Finset.range (H + 1), 3 ^ (-(1 / 2 - rhoMax) * ↑r)

theorem HCPolySupport.HighContrast.Response.centeredWindowCoefficient_eq (H : ℕ) (rhoMax : ℝ) : centeredWindowCoefficient H rhoMax = 2 * ∑ r ∈ Finset.range (H + 1), 3 ^ (-(1 / 2 - rhoMax) * ↑r)

The defining equation for S_cen.

noncomputable def HCPolySupport.HighContrast.Response.nonlinearCellWindowCoefficient (H : ℕ) (a Q : ℝ) : ℝ

The finite nonlinear cell coefficient S_nl^cell.

Equations

• HCPolySupport.HighContrast.Response.nonlinearCellWindowCoefficient H a Q = ∑ r ∈ Finset.Icc 1 H, 3 ^ (-↑r / 2 + a * (↑r - 1) / Q)

noncomputable def HCPolySupport.HighContrast.Response.nonlinearAverageWindowCoefficient (H : ℕ) (a Q : ℝ) : ℝ

The finite nonlinear averaged-defect coefficient S_nl^av.

Equations

• HCPolySupport.HighContrast.Response.nonlinearAverageWindowCoefficient H a Q = ∑ r ∈ Finset.Icc 1 H, 3 ^ (-a * ↑r + a * (↑r - 1) / (2 * Q))

noncomputable def HCPolySupport.HighContrast.Response.constantSeminormCoefficient : ℝ

The constant contribution c_const = (1 - 3⁻¹_right²)⁻¹.

Equations

• HCPolySupport.HighContrast.Response.constantSeminormCoefficient = (1 - 3 ^ (-1 / 2))⁻¹

theorem HCPolySupport.HighContrast.Response.constantSeminormCoefficient_eq : constantSeminormCoefficient = (1 - 3 ^ (-1 / 2))⁻¹

The defining equation for c_const.

noncomputable def HCPolySupport.HighContrast.Response.profileEnergyLoad {d : ℕ} (L : ℝ) (p q : Vec d) : ℝ

The response-energy load Λ_t = ((L_t)^2 + |p·q|)¹_right².

Equations

• HCPolySupport.HighContrast.Response.profileEnergyLoad L p q = √(L ^ 2 + |HCPolySupport.vecDot p q|)

theorem HCPolySupport.HighContrast.Response.profileEnergyLoad_eq {d : ℕ} (L : ℝ) (p q : Vec d) : profileEnergyLoad L p q = √(L ^ 2 + |vecDot p q|)

The defining equation for Λ_t.

theorem HCPolySupport.HighContrast.Response.profileEnergyLoad_nonneg {d : ℕ} (L : ℝ) (p q : Vec d) : 0 ≤ profileEnergyLoad L p q