MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiSection13QhatMajorantInternal

source

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_normalizedMinusBase_continuousOn_compact {H : Section13HatLayers} (hH : Section13HatSourceContract H) (S : ℝ) :

ContinuousOn (Section10Lemma1028FirstCrossing.normalizedMinusBase (section13Qhat H) Section10CanonicalXi.xi) (Set.Icc 3 S)

Inspect dependencies

MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_normalizedMinusBase_continuousOn_compact · compiled type and proof/definition references.

source

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_minusMajorant_internal {H : Section13HatLayers} (hH : Section13HatSourceContract H) :

Section10Equation1056UniformStationary.QhatMinusMajorant (section13Qhat H)

Equations

MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_minusMajorant_internal hH = Section10Equation1056UniformStationary.qhatMinusMajorant_of_uniform_stationary (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13QhatMajorantClosure.section13QhatFirstCrossingData hH) ⋯ (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_lemma1027AdjointRComparison hH) MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_minusMajorant_internal._proof_3 ⋯

Instances For

Inspect dependencies

MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_minusMajorant_internal · compiled type and proof/definition references.

source

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_cutoffMajorant_internal {H : Section13HatLayers} (hH : Section13HatSourceContract H) :

CutoffCorrectedRatio.CutoffMajorant (section13Qhat H)

Equations

MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_cutoffMajorant_internal hH = { xi := Section10CanonicalXi.xi, cMinus := (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_minusMajorant_internal hH).cMinus, cutoff := (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_minusMajorant_internal hH).cutoff, A := (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_minusMajorant_internal hH).A, four_le_cutoff := ⋯, one_le_A := ⋯, majorizes_log := ⋯, envelope_slope_nonpos := ⋯ }

Instances For

Inspect dependencies

MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat_cutoffMajorant_internal · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.moving_claim14_6_iii_of_section13HatSourceContract {H : Section13HatLayers} (hH : Section13HatSourceContract H) {d Δ : ℝ} (hd : 0 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) :

Section13MajorantsFinal.MovingClaim146iiiConclusion H d Δ

Fully internalized moving Claim 14.6(iii): the only mathematical input is Section 13's source contract, including its genuine (T5) exponential decay.

Inspect dependencies

MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.moving_claim14_6_iii_of_section13HatSourceContract · compiled type and proof/definition references.