Documentation

LeanPool.HighContrastHomogenization.Entry.Response.Kernel.EtaKernelBound

High-contrast homogenization: Entry.Response.Kernel.EtaKernelBound #

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

The η-kernel bound #

This is the η-kernel of the diagonal weak-norm estimate (p.response.transfer): for each depth n and index w, the two-sided normalized recent defect satisfies ∫ ‖D_{n,w}‖² ≤ K_n η^{2/Q} once the two-sided smallness hypothesis ∫ respAllScaleAbs^Q dP ≤ Cm η is supplied together with its measurability and integrability. This file discharges both premises from RawOutput, RespCalibrated and RespSourceSmall alone, so that the two corollaries below need no further analytic input.

source
theorem HCPolySupport.HighContrast.Multiscale.integral_recentDefect_sq_le_minus (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) (Cc Cm : ℝ) (hCc : 0 < Cc) (hCm : 0 < Cm) :
∃ (K : ℕ → ℝ), (∀ (n : ℕ), 0 < K n) ∧ ∀ (ε σ 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 → ∀ η ∈ Set.Ioo 0 (1 / 2), MeasureTheory.Integrable (fun (a : CoeffSpace d) => respAllScaleAbs P γ jStar F t a ^ bigQ d γ) P → ∫ (a : CoeffSpace d), respAllScaleAbs P γ jStar F t a ^ bigQ d γ ∂P ≤ Cm * η → ∀ (n : ℕ), ∀ w ∈ triadicIndexBox d n, MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => recentDefectBlock (respGrid jStar F) t n w (respEhatMinus P jStar F t) (respCoeffMinus F a)) P ∧ MeasureTheory.Integrable (fun (a : CoeffSpace d) => recentDefect (respGrid jStar F) t n w (respEhatMinus P jStar F t) (respCoeffMinus F a) ^ 2) P ∧ ∫ (a : CoeffSpace d), recentDefect (respGrid jStar F) t n w (respEhatMinus P jStar F t) (respCoeffMinus F a) ^ 2 ∂P ≤ K n * η ^ (2 / ↑(bigQ d γ))

The η-kernel (paper p.response.transfer). For each depth n and index w, the two-sided normalized recent defect is square-integrable with ∫ ‖D_{n,w}‖^2 ≤ K_n η^{2/Q}.

The smallness hypothesis is the TWO-SIDED ∫ respAllScaleAbs ^ Q ∂P ≤ Cm * η, not the one-sided respAllScaleMax one. The conclusion K n * η ^ (2/Q) and every other binder are unchanged. The η-kernel obstruction shows that the one-sided hypothesis implies the conclusion for NO constant sequence K; the paper routes this step through the two-sided fluctuation history, not through M (p.response.transfer). The two-sided premise is carried by an L² quantity and is discharged through blockOpNorm (normalizedFluctuation …).

The lower side needs a pathwise lower Loewner bound. The deterministic block-algebra identities swapConj_lowerRight / schurSigma_le_corrected / meanPenalty concern a single symmetric positive definite E; they mention neither the sample a nor the cell, so they cannot produce that bound. The route is:

  • D_{n,w} = (N_{n,w} - I) - (N_0 - I) with N = normalizedBlock(·, E_t), using normalizedBlock_blockSub and adaptedCellAtCenter_zero;
  • both summands are bounded by respAllScaleAbs through le_csSup (weights 3^{ρn} and 1), so ‖D_{n,w}‖ ≤ (3^{ρn} + 1) · respAllScaleAbs a -- this is the step the one-sided carrier could not supply;
  • the recentred field a_∓ and the normalizer Ehat^∓ = blockCongr (respG F) E_t are the SAME congruence of the E_t-picture (coarseBlockMatrix_respCoeffMinus_at / _respCoeffPlus_at below), and a congruence applied to both the block and its normalizer leaves the normalized block orthogonally similar, hence leaves blockOpNorm unchanged;
  • Jensen on the probability measure with Q ≥ 2 then gives ∫ D^2 ≤ (3^{ρn}+1)^2 (Cm η)^{2/Q}, i.e. K n := (3^{ρn}+1)^2 · Cm^{2/Q} > 0.

Conjunct 1 (measurability) is aestronglyMeasurable_recentDefectBlock_minus/plus above, carrier-independent. Conjunct 2 is the same pointwise bound.

All three conjuncts, both signs. K n := (3 ^ (Quenched.contrastRho γ * n) + 1) ^ 2 * Cm ^ (2/Q), positive. The chain above:

  • blockSpecBound_le_blockOpNorm -- blockSpecBound N ≤ blockOpNorm N UNCONDITIONALLY, so the new hypothesis implies the old one and no respAllScaleMax consumer is lost;
  • blockOpNorm_sub_id_le_specBound_add_two and pathwise_envelope_abs -- the two-sided defining set is a.e. BddAbove, the respAllScaleAbs analogue;
  • weighted_blockOpNorm_le_respAllScaleAbs -- the le_csSup step;
  • blockOpNorm_normalizedBlock_sub_le -- the split (N_{n,w} - I) - (N_0 - I) in the E_t-picture, which is where BOTH sides are needed and where the one-sided carrier fails;
  • blockOpNorm_normalizedBlock_blockCongr_le -- congruence invariance: U = matSqrt E · G · matSqrt (Gᵀ E G)⁻¹ has Uᵀ U = 1, so applying the same blockCongr to a block and to its normalizer leaves the normalized block orthogonally similar;
  • blockCongr_posDef (with isUnit_respG / isUnit_respGPlus) -- positive definiteness of Ehat^∓, discharged, not assumed;
  • recentDefect_le_respAllScaleAbs_minus / _plus -- THE η-KERNEL POINTWISE BOUND, recentDefect ≤ (3 ^ (ρ n) + 1) · respAllScaleAbs a a.e., uniformly in n and w;
  • respAllScaleAbs_measurable, respAllScaleAbs_nonneg, integral_sq_le_rpow (Jensen, ∫ f ^ 2 ≤ (∫ f ^ Q) ^ (2/Q) on a probability measure) and conjuncts_of_pointwise -- integrability (conjunct 2) and the exponent (conjunct 3).

Conjunct 1 is aestronglyMeasurable_recentDefectBlock_minus / _plus, carrier-independent.

source
theorem HCPolySupport.HighContrast.Multiscale.integral_recentDefect_sq_le_plus (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) (Cc Cm : ℝ) (hCc : 0 < Cc) (hCm : 0 < Cm) :
∃ (K : ℕ → ℝ), (∀ (n : ℕ), 0 < K n) ∧ ∀ (ε σ 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 → ∀ η ∈ Set.Ioo 0 (1 / 2), MeasureTheory.Integrable (fun (a : CoeffSpace d) => respAllScaleAbs P γ jStar F t a ^ bigQ d γ) P → ∫ (a : CoeffSpace d), respAllScaleAbs P γ jStar F t a ^ bigQ d γ ∂P ≤ Cm * η → ∀ (n : ℕ), ∀ w ∈ triadicIndexBox d n, MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => recentDefectBlock (respGrid jStar F) t n w (respEhatPlus P jStar F t) (respCoeffPlus F a)) P ∧ MeasureTheory.Integrable (fun (a : CoeffSpace d) => recentDefect (respGrid jStar F) t n w (respEhatPlus P jStar F t) (respCoeffPlus F a) ^ 2) P ∧ ∫ (a : CoeffSpace d), recentDefect (respGrid jStar F) t n w (respEhatPlus P jStar F t) (respCoeffPlus F a) ^ 2 ∂P ≤ K n * η ^ (2 / ↑(bigQ d γ))

The η-kernel, plus sign.

The η-kernel twins reduced to the source hypotheses #

Both premises of the twins above -- Integrable (fun a => respAllScaleAbs ^ Q) P and ∫ respAllScaleAbs ^ Q ∂P ≤ Cm η -- are supplied by respAllScaleAbs_aestronglyMeasurable_integrable (above) and response_allscale_abs . The two corollaries below discharge both premises and leave only RawOutput, RespCalibrated, RespSourceSmall and the profile smallness Cprof σ^{(1-γ)/8} ≤ η -- exactly the premises the assembly already supplies to response_allscale_abs and response_source_smallness (AdaptedResponseAssembly.lean). They show that the wiring closes: Cm is no longer a free constant of the twins but the C produced by response_allscale_abs, and the two Csrcs are reconciled by the tree's max idiom, as AdaptedResponseAssembly.lean does.

source
theorem HCPolySupport.HighContrast.Multiscale.integral_recentDefect_sq_le_of_rawOutput_minus (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) (Cc : ℝ) (hCc : 0 < Cc) (Cs : ℝ) (hCs : 0 < Cs) :
∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (K : ℕ → ℝ), (∀ (n : ℕ), 0 < K n) ∧ ∀ (ε σ : ℝ), ε ∈ Set.Ioc 0 S.eps0 → σ ∈ Set.Ioc 0 ε → ∀ (Cglob Cprof Bresp : ℝ), 0 ≤ Cglob → ∀ (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 → ∀ η ∈ Set.Ioo 0 (1 / 2), Cprof * σ ^ ((1 - γ) / 8) ≤ η → RespSourceSmall d γ Cs η E F jStar s t → ∀ (n : ℕ), ∀ w ∈ triadicIndexBox d n, MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => recentDefectBlock (respGrid jStar F) t n w (respEhatMinus P jStar F t) (respCoeffMinus F a)) P ∧ MeasureTheory.Integrable (fun (a : CoeffSpace d) => recentDefect (respGrid jStar F) t n w (respEhatMinus P jStar F t) (respCoeffMinus F a) ^ 2) P ∧ ∫ (a : CoeffSpace d), recentDefect (respGrid jStar F) t n w (respEhatMinus P jStar F t) (respCoeffMinus F a) ^ 2 ∂P ≤ K n * η ^ (2 / ↑(bigQ d γ))

The η-kernel wired, minus sign. The conclusion of integral_recentDefect_sq_le_minus with both respAllScaleAbs premises discharged from RawOutput by response_allscale_abs and respAllScaleAbs_aestronglyMeasurable_integrable.

source
theorem HCPolySupport.HighContrast.Multiscale.integral_recentDefect_sq_le_of_rawOutput_plus (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) (Cc : ℝ) (hCc : 0 < Cc) (Cs : ℝ) (hCs : 0 < Cs) :
∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (K : ℕ → ℝ), (∀ (n : ℕ), 0 < K n) ∧ ∀ (ε σ : ℝ), ε ∈ Set.Ioc 0 S.eps0 → σ ∈ Set.Ioc 0 ε → ∀ (Cglob Cprof Bresp : ℝ), 0 ≤ Cglob → ∀ (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 → ∀ η ∈ Set.Ioo 0 (1 / 2), Cprof * σ ^ ((1 - γ) / 8) ≤ η → RespSourceSmall d γ Cs η E F jStar s t → ∀ (n : ℕ), ∀ w ∈ triadicIndexBox d n, MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => recentDefectBlock (respGrid jStar F) t n w (respEhatPlus P jStar F t) (respCoeffPlus F a)) P ∧ MeasureTheory.Integrable (fun (a : CoeffSpace d) => recentDefect (respGrid jStar F) t n w (respEhatPlus P jStar F t) (respCoeffPlus F a) ^ 2) P ∧ ∫ (a : CoeffSpace d), recentDefect (respGrid jStar F) t n w (respEhatPlus P jStar F t) (respCoeffPlus F a) ^ 2 ∂P ≤ K n * η ^ (2 / ↑(bigQ d γ))

The η-kernel wired, plus sign. The plus twin of integral_recentDefect_sq_le_of_rawOutput_minus.

Local helper for the squared recent sums #

source
theorem HCPolySupport.HighContrast.Multiscale.integral_weakSums_sq_le {d : ℕ} (rho : ℝ) (hrho : 0 ≤ rho) (K : ℕ → ℝ) (hK : ∀ (n : ℕ), 0 < K n) (Q : ℕ) (hQ : 1 ≤ Q) :
∃ (D : ℕ → ℝ), (∀ (H : ℕ), 0 < D H) ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (q : Mat d) (t : ℤ) (H : ℕ) (E : BlockMat d) (b : CoeffSpace d → CoeffField d), ∀ η ∈ Set.Ioo 0 (1 / 2), (∀ n ≤ H, ∀ w ∈ triadicIndexBox d n, MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => recentDefectBlock q t n w E (b a)) P ∧ MeasureTheory.Integrable (fun (a : CoeffSpace d) => recentDefect q t n w E (b a) ^ 2) P ∧ ∫ (a : CoeffSpace d), recentDefect q t n w E (b a) ^ 2 ∂P ≤ K n * η ^ (2 / ↑Q)) → MeasureTheory.Integrable (fun (a : CoeffSpace d) => (weakCellSum q t H E (b a) + weakAverageSum q t H rho E (b a)) ^ 2) P ∧ ∫ (a : CoeffSpace d), (weakCellSum q t H E (b a) + weakAverageSum q t H rho E (b a)) ^ 2 ∂P ≤ D H * η ^ (1 / ↑Q)

Bookkeeping from the η-kernel to the squared recent sums (p.response.transfer, finite window n ≤ H): (S_cell + S_av)^2 ≤ 2S_cell^2 + 2S_av^2; Cauchy–Schwarz on the finite sums; S_cell: ∫ weakCellDefect^2 = avg_w ∫ ‖D_{n,w}‖^2 ≤ K_n η^{2/Q} ≤ K_n η^{1/Q} (η < 1); S_av: ‖avg_w D‖ ≤ avg_w ‖D‖ ≤ (avg_w ‖D‖^2)^{1/2} (ofFullBlockMat/toFullBlockMat inverse, norm of a mean) and ∫ √f ≤ (∫ f)^{1/2} on a probability measure, giving √K_n η^{1/Q}. D H = 2(H+1) ∑_{n ≤ H} (K n + √(K n)) + 1 works.