UpperAfterBandConsumption

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarAfterBandCoordinateLane {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (E : ℝ) (j : Fin d) (omega : Cutoff.CutoffSample d) : ℝ

The tuned collar after-band coordinate lane at a strict descendant.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarAfterBandTraceLane {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (E : ℝ) (omega : Cutoff.CutoffSample d) : ℝ

The literal finite-coordinate collar after-band trace.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarAfterBandCoordinateLane_nonneg {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (E : ℝ) (j : Fin d) (omega : Cutoff.CutoffSample d) : 0 ≤ probeSharpFramedCollarAfterBandCoordinateLane M m R E j omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.measurable_probeSharpFramedCollarAfterBandCoordinateLane {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (E : ℝ) (j : Fin d) : Measurable (probeSharpFramedCollarAfterBandCoordinateLane M m R E j)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarAfterBandCoordinateLane_eq {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (E : ℝ) (j j' : Fin d) : probeSharpFramedCollarAfterBandCoordinateLane M m R E j = probeSharpFramedCollarAfterBandCoordinateLane M m R E j'

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarAfterBandTraceLane_eq_dimension_mul {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (E : ℝ) (j : Fin d) (omega : Cutoff.CutoffSample d) : probeSharpFramedCollarAfterBandTraceLane M m R E omega = ↑d * probeSharpFramedCollarAfterBandCoordinateLane M m R E j omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedCollarAfterBandTraceLane_nonneg {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (E : ℝ) (omega : Cutoff.CutoffSample d) : 0 ≤ probeSharpFramedCollarAfterBandTraceLane M m R E omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.measurable_probeSharpFramedCollarAfterBandTraceLane {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (E : ℝ) : Measurable (probeSharpFramedCollarAfterBandTraceLane M m R E)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collar_afterBand_trace_isBigOWith_depthProfile {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : { E : ℝ // 1 ≤ E }} (hstate : Frozen.Section3.inductionState M (m - 1) E) {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) : have k₀ := collarBandMeanDepth M ↑E; have rho := 3 ^ (-(1 / 40)); have F := Multiscale.probeMeanGoodWaveConst M * (5 * ↑d ^ 2) * (4 * Affine.superposedGradConst d ^ 2 * probeSharpCollarBandMeanCapQuarter M (↑E) k₀ * probeSharpCollarBandMeanMassQuarterConst d * 3 ^ (2 * bfaProfileB * ↑k₀) * 3 ^ (1 / 16)); have A₀ := F * (64 * superposedFluxHsepConst ^ 3 * (54 * Multiscale.waveSharpUpperConst d ^ 2)); have target := min 1 (M.gamma * ↑(k + 1)) * 3 ^ (M.gamma * ↑(k + 1)); (∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ENNReal.ofReal (probeSharpFramedCollarAfterBandTraceLane M m R (↑E) omega) = ∑ j : Fin d, ∑' (n : ℕ), ENNReal.ofReal (Multiscale.probeSharpFramedCollarWavePart M R.scale (↑E) bfaProfileB k₀ n (m - 1) (HCPolySupport.basisVec j) (Affine.superposedGradConst d) (fun (eta : Cutoff.CutoffSample d) => probeSharpAfterBandTerm M R.scale (probeSharpLayerAnchor R.scale bfaProfileB k₀ n) k₀ m eta ^ 2) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega))) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (upperProfileTargetSigma sigma)) (probeSharpFramedCollarAfterBandTraceLane M m R ↑E) (↑d * (HCPolySupport.IndependentSums.gammaTriangleConst (upperProfileTargetSigma sigma) * ((A₀ * ∑' (n : ℕ), ↑(n + 1) * rho ^ n) * target)))

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.collarAfterBandTunedTracePrefactor (d : ℕ) : ℝ

Dimension-only prefactor after extracting the tuned collar cap.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.collarAfterBandTunedOutputConst (d : ℕ) : ℝ

Threshold paying the tuned decay and eighth-power reserve.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collar_afterBand_trace_isBigOWith_frozenReserve {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : { E : ℝ // 1 ≤ E }} (hstate : Frozen.Section3.inductionState M (m - 1) E) {sigma Cup : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hmax : max (Real.exp (Cup / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) (hOutput : max (profileAuxiliaryConst d) (collarAfterBandTunedOutputConst d) ≤ Cup) : have eps := Real.exp (-(Cup⁻¹ * ((↑E)⁻¹ ^ 2 * M.gamma⁻¹))); (∀ (omega : Cutoff.CutoffSample d), 0 ≤ probeSharpFramedCollarAfterBandTraceLane M m R (↑E) omega) ∧ Measurable (probeSharpFramedCollarAfterBandTraceLane M m R ↑E) ∧ (∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ENNReal.ofReal (probeSharpFramedCollarAfterBandTraceLane M m R (↑E) omega) = ∑ j : Fin d, ∑' (n : ℕ), ENNReal.ofReal (Multiscale.probeSharpFramedCollarWavePart M R.scale (↑E) bfaProfileB (collarBandMeanDepth M ↑E) n (m - 1) (HCPolySupport.basisVec j) (Affine.superposedGradConst d) (fun (eta : Cutoff.CutoffSample d) => probeSharpAfterBandTerm M R.scale (probeSharpLayerAnchor R.scale bfaProfileB (collarBandMeanDepth M ↑E) n) (collarBandMeanDepth M ↑E) m eta ^ 2) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega))) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (upperProfileTargetSigma sigma)) (probeSharpFramedCollarAfterBandTraceLane M m R ↑E) (3 ^ (M.gamma * (↑k + 1)) * eps ^ 8)