def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.SourceCutoffLogDomination (K A d M : ℝ) : Prop

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.SourceCutoffLogDomination K A d M = (0 < d ∧ 1 < M ∧ ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → M ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d ∧ ∀ (t : ℝ), M ≤ t → t ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d → 2 * (d + 1) * K ^ 2 * A * max 1 (Real.log (1 + t ^ d / Real.log D)) ≤ Real.log (Real.exp 1 * t))

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_sourceCutoffLogDomination {K A d : ℝ} (hd : 0 < d) (hK : 1 ≤ K) (hA : 1 ≤ A) : ∃ (M : ℝ), SourceCutoffLogDomination K A d M

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131MovingDelayedCurrentRatioOnSource_mono {H : Section13HatLayers} (sign : ErrorSign) {d M₀ M : ℝ} (hd : 0 < d) (hM : M₀ ≤ M) (hratio : SourceClaim146AssemblyNext.Proposition131MovingDelayedCurrentRatioOnSource H sign d M₀) : SourceClaim146AssemblyNext.Proposition131MovingDelayedCurrentRatioOnSource H sign d M

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_ratioOnSource_of_cutoffMajorant {H : Section13HatLayers} (hH : Section13HatSourceContract H) (sign : ErrorSign) {d : ℝ} (hd : 0 < d) (majorant : CutoffCorrectedRatio.CutoffMajorant (BridgeAssembly.section13_bridgeAtThree hH sign).Qhat) : ∃ (M : ℝ), SourceClaim146AssemblyNext.Proposition131MovingDelayedCurrentRatioOnSource H sign d M

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_common_ratioOnSource_of_cutoffMajorants {H : Section13HatLayers} (hH : Section13HatSourceContract H) {d : ℝ} (hd : 0 < d) (majorant : (sign : ErrorSign) → CutoffCorrectedRatio.CutoffMajorant (BridgeAssembly.section13_bridgeAtThree hH sign).Qhat) : ∃ (M : ℝ), 1 < M ∧ ∀ (sign : ErrorSign), SourceClaim146AssemblyNext.Proposition131MovingDelayedCurrentRatioOnSource H sign d M

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.eventually_movingSigma_large_s_differential_tail_onSource_strict {H : Section13HatLayers} (hH : Section13HatContract H 2) (sign : ErrorSign) {d Δ M : ℝ} (hM : 4 ≤ M) (hΔ : Δ < 1) (hcert : MovingDDEAsymptoticCertificateOnSource H sign d M) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → M ≤ sourceSigma D d ∧ ∀ (s : ℝ), M ≤ s → s ≤ sourceSigma D d → ∫ (t : ℝ) in s..sourceSigma D d, qD H sign.opposite D d Δ t < (1 - 1 / sourceSigma D d) ^ (1 - Δ) * lambda H sign D d 0 s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.moving_claim14_6_iii_of_source_contract_and_cutoffMajorants {H : Section13HatLayers} (hH : Section13HatSourceContract H) {d Δ : ℝ} (hd : 0 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (majorant : (sign : ErrorSign) → CutoffCorrectedRatio.CutoffMajorant (BridgeAssembly.section13_bridgeAtThree hH sign).Qhat) : ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (sign : ErrorSign) (s : ℝ), 2 + sign.epsilon ≤ s → s ≤ sourceSigma D d → ∫ (t : ℝ) in s..sourceSigma D d, qD H sign.opposite D d Δ t < (1 - 1 / sourceSigma D d) ^ (1 - Δ) * lambda H sign D d 0 s