Source indexedlemma · leanprover/lean4:v4.32.0

hasProd_norm_inv_le_exp_of_pointwise_le_exp

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanProductBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanProductBound.lean:81 to 103

Mathematical statement

Exact Lean statement

lemma hasProd_norm_inv_le_exp_of_pointwise_le_exp {α : Type} {fac : α → ℂ} {F : ℂ}
    (hfac : HasProd fac F (SummationFilter.unconditional α))
    (b : α → ℝ) (B : ℝ)
    (hterm : ∀ x, ‖(fac x)⁻¹‖ ≤ Real.exp (b x))
    (hsum : ∀ s : Finset α, (∑ x ∈ s, b x) ≤ B) :
    ‖F⁻¹‖ ≤ Real.exp B

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma hasProd_norm_inv_le_exp_of_pointwise_le_exp {α : Type} {fac : α → ℂ} {F : ℂ}    (hfac : HasProd fac F (SummationFilter.unconditional α))    (b : α → ℝ) (B : ℝ)    (hterm : ∀ x, ‖(fac x)⁻¹‖ ≤ Real.exp (b x))    (hsum : ∀ s : Finset α, (∑ x ∈ s, b x) ≤ B) :    ‖F⁻¹‖ ≤ Real.exp B := by  by_cases hF : F = 0  · subst hF    simpa using exp_nonneg B  have hnorm :      HasProd (fun x => ‖(fac x)⁻¹‖) ‖F⁻¹‖ (SummationFilter.unconditional α) :=    hasProd_norm_inv_unconditional hfac hF  have hprod : ∀ s : Finset α, (∏ x ∈ s, ‖(fac x)⁻¹‖) ≤ Real.exp B := by    intro s    have h0 : ∀ x ∈ s, 0 ≤ ‖(fac x)⁻¹‖ := by intro _ _; positivity    have h1 : (∏ x ∈ s, ‖(fac x)⁻¹‖) ≤ Real.exp (∑ x ∈ s, b x) := by      refine Finset.prod_le_exp_sum s (a := fun x => ‖(fac x)⁻¹‖) (b := b) h0 ?_      intro x hx      simpa using hterm x    have h2 : Real.exp (∑ x ∈ s, b x) ≤ Real.exp B :=      Real.exp_le_exp.2 (hsum s)    exact h1.trans h2  exact hasProd_le_of_prod_le_exp hnorm hprod