Source indexedlemma · leanprover/lean4:v4.32.0

Complex.Hadamard.card_subtype_le_divisorMassClosedBall₀_of_norm_le

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Summability.lean:334 to 359

Source documentation

A finite family of divisor indices contained in a closed ball has cardinality bounded by the divisor mass of that ball.

Exact Lean statement

lemma card_subtype_le_divisorMassClosedBall₀_of_norm_le
    {f : ℂ → ℂ} (hf : Differentiable ℂ f)
    {s : Set (divisorZeroIndex₀ f (Set.univ : Set ℂ))} [Fintype s]
    {R : ℝ} (hR : 0 < R) (hs : ∀ p : s, ‖divisorZeroIndex₀_val p.1‖ ≤ R) :
    (Fintype.card s : ℝ) ≤ divisorMassClosedBall₀ f R

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma card_subtype_le_divisorMassClosedBall₀_of_norm_le    {f : ℂ → ℂ} (hf : Differentiable ℂ f)    {s : Set (divisorZeroIndex₀ f (Set.univ : Set ℂ))} [Fintype s]    {R : ℝ} (hR : 0 < R) (hs : ∀ p : s, ‖divisorZeroIndex₀_val p.1‖ ≤ R) :    (Fintype.card s : ℝ) ≤ divisorMassClosedBall₀ f R := by  let Aball : Type :=    {p : divisorZeroIndex₀ f (Set.univ : Set ℂ) // ‖divisorZeroIndex₀_val p‖ ≤ R}  haveI : Fintype Aball := by    have : Finite Aball := by      have : Metric.closedBall (0 : ℂ) R ⊆ (Set.univ : Set ℂ) := by simp      simpa [Aball] using        (finite_divisorZeroIndex₀_subtype_norm_le (f := f) (U := (Set.univ : Set ℂ))          (B := R) this)    exact Fintype.ofFinite _  have hinj : Function.Injective (fun p : s => (⟨p.1, hs p⟩ : Aball)) := by    intro p q hpq    apply Subtype.ext    exact congrArg (fun x : Aball => x.1) hpq  have hcard_le : Fintype.card s ≤ Fintype.card Aball :=    Fintype.card_le_of_injective _ hinj  have hAball : (Nat.card Aball : ℝ) ≤ divisorMassClosedBall₀ f R := by    simpa [Aball] using card_ball_le_divisorMassClosedBall₀ (f := f) hf hR  calc    (Fintype.card s : ℝ) ≤ (Fintype.card Aball : ℝ) := by exact_mod_cast hcard_le    _ = (Nat.card Aball : ℝ) := by simp [Nat.card_eq_fintype_card]    _ ≤ divisorMassClosedBall₀ f R := hAball