theorem aux1 {d : ℕ} (S : PeriodicSpherePacking d) (D : Set (EuclideanSpace ℝ (Fin d))) (hD_isBounded : Bornology.IsBounded D) : Bornology.IsBounded (⋃ x ∈ S.centers ∩ D, Metric.ball x (S.separation / 2))

theorem aux2 {d : ℕ} (S : PeriodicSpherePacking d) (D : Set (EuclideanSpace ℝ (Fin d))) : (S.centers ∩ D).PairwiseDisjoint fun (x : EuclideanSpace ℝ (Fin d)) => Metric.ball x (S.separation / 2)

theorem aux3 {ι : Type u_1} {τ : Type u_2} {s : Set ι} {f : ι → Set (EuclideanSpace ℝ τ)} {c : ENNReal} (hc : 0 < c) [Fintype τ] [MeasureTheory.NoAtoms MeasureTheory.volume] (h_measurable : ∀ x ∈ s, MeasurableSet (f x)) (h_bounded : Bornology.IsBounded (⋃ x ∈ s, f x)) (h_volume : ∀ x ∈ s, c ≤ MeasureTheory.volume (f x)) (h_disjoint : s.PairwiseDisjoint f) : s.Finite

theorem aux4 {d : ℕ} (S : PeriodicSpherePacking d) (D : Set (EuclideanSpace ℝ (Fin d))) (hD_isBounded : Bornology.IsBounded D) (hd : 0 < d) : Finite ↑(S.centers ∩ D)

theorem aux4' {d : ℕ} (S : PeriodicSpherePacking d) {ι : Type u_1} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) (hd : 0 < d) : Finite ↑(S.centers ∩ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b))

theorem aux4'' {d : ℕ} (S : PeriodicSpherePacking d) {ι : Type u_1} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) (hd : 0 < d) (v : EuclideanSpace ℝ (Fin d)) : Finite ↑(S.centers ∩ (v +ᵥ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b)))

theorem PeriodicSpherePacking.fract_centers {d : ℕ} (S : PeriodicSpherePacking d) {ι : Type u_1} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) (s : ↑S.centers) : ZSpan.fract (Basis.ofZLatticeBasis ℝ S.lattice b) ↑s ∈ S.centers

theorem PeriodicSpherePacking.orbitRel_fract {d : ℕ} (S : PeriodicSpherePacking d) {ι : Type u_1} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) (a : ↑S.centers) : (AddAction.orbitRel ↥S.lattice ↑S.centers) ⟨ZSpan.fract (Basis.ofZLatticeBasis ℝ S.lattice b) ↑a, ⋯⟩ a

noncomputable def PeriodicSpherePacking.addActionOrbitRelEquiv {d : ℕ} (S : PeriodicSpherePacking d) (D : Set (EuclideanSpace ℝ (Fin d))) (hD_unique_covers : ∀ (x : EuclideanSpace ℝ (Fin d)), ∃! g : ↥S.lattice, g +ᵥ x ∈ D) : Quotient (AddAction.orbitRel ↥S.lattice ↑S.centers) ≃ ↑(S.centers ∩ D)

Equations

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

noncomputable def PeriodicSpherePacking.addActionOrbitRelEquiv' {d : ℕ} (S : PeriodicSpherePacking d) {ι : Type u_1} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) : Quotient (AddAction.orbitRel ↥S.lattice ↑S.centers) ≃ ↑(S.centers ∩ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b))

Equations

• S.addActionOrbitRelEquiv' b = S.addActionOrbitRelEquiv (ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b)) ⋯

noncomputable def PeriodicSpherePacking.addActionOrbitRelEquiv'' {d : ℕ} (S : PeriodicSpherePacking d) {ι : Type u_1} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) (v : EuclideanSpace ℝ (Fin d)) : Quotient (AddAction.orbitRel ↥S.lattice ↑S.centers) ≃ ↑(S.centers ∩ (v +ᵥ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b)))

Equations

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

instance instSubsingletonElemEuclideanSpaceRealFinOfNatNatCenters (S : PeriodicSpherePacking 0) : Subsingleton ↑S.centers

instance instFiniteElemEuclideanSpaceRealFinOfNatNatCenters (S : PeriodicSpherePacking 0) : Finite ↑S.centers

instance PeriodicSpherePacking.finiteOrbitRelQuotient {d : ℕ} (S : PeriodicSpherePacking d) : Finite (Quotient (AddAction.orbitRel ↥S.lattice ↑S.centers))

noncomputable instance instFintypeQuotientElemEuclideanSpaceRealFinCentersOrbitRelSubtypeMemSubmoduleIntLattice {d : ℕ} (S : PeriodicSpherePacking d) : Fintype (Quotient (AddAction.orbitRel ↥S.lattice ↑S.centers))

Equations

• instFintypeQuotientElemEuclideanSpaceRealFinCentersOrbitRelSubtypeMemSubmoduleIntLattice S = Fintype.ofFinite (Quotient (AddAction.orbitRel ↥S.lattice ↑S.centers))

noncomputable instance PeriodicSpherePacking.instCentersSetoid {d : ℕ} (S : PeriodicSpherePacking d) : Setoid ↑S.centers

Equations

• S.instCentersSetoid = AddAction.orbitRel ↥S.lattice ↑S.centers

noncomputable def PeriodicSpherePacking.numReps {d : ℕ} (S : PeriodicSpherePacking d) : ℕ

Equations

• S.numReps = Fintype.card (Quotient (AddAction.orbitRel ↥S.lattice ↑S.centers))

theorem PeriodicSpherePacking.numReps_eq_one {d : ℕ} (S : PeriodicSpherePacking d) (hS : S.centers = ↑S.lattice) : S.numReps = 1

theorem PeriodicSpherePacking.card_centers_inter_isFundamentalDomain {d : ℕ} (S : PeriodicSpherePacking d) (D : Set (EuclideanSpace ℝ (Fin d))) (hD_isBounded : Bornology.IsBounded D) (hD_unique_covers : ∀ (x : EuclideanSpace ℝ (Fin d)), ∃! g : ↥S.lattice, g +ᵥ x ∈ D) (hd : 0 < d) : (S.centers ∩ D).toFinset.card = S.numReps

theorem PeriodicSpherePacking.encard_centers_inter_isFundamentalDomain {d : ℕ} (S : PeriodicSpherePacking d) (D : Set (EuclideanSpace ℝ (Fin d))) (hD_isBounded : Bornology.IsBounded D) (hD_unique_covers : ∀ (x : EuclideanSpace ℝ (Fin d)), ∃! g : ↥S.lattice, g +ᵥ x ∈ D) (hd : 0 < d) : (S.centers ∩ D).encard = ↑S.numReps

theorem PeriodicSpherePacking.card_centers_inter_fundamentalDomain {d : ℕ} (S : PeriodicSpherePacking d) (hd : 0 < d) {ι : Type u_1} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) : (S.centers ∩ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b)).toFinset.card = S.numReps

theorem PeriodicSpherePacking.encard_centers_inter_fundamentalDomain {d : ℕ} (S : PeriodicSpherePacking d) (hd : 0 < d) {ι : Type u_1} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) : (S.centers ∩ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b)).encard = ↑S.numReps

theorem PeriodicSpherePacking.card_centers_inter_vadd_fundamentalDomain {d : ℕ} (S : PeriodicSpherePacking d) (hd : 0 < d) {ι : Type u_1} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) (v : EuclideanSpace ℝ (Fin d)) : (S.centers ∩ (v +ᵥ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b))).toFinset.card = S.numReps

theorem PeriodicSpherePacking.encard_centers_inter_vadd_fundamentalDomain {d : ℕ} (S : PeriodicSpherePacking d) (hd : 0 < d) {ι : Type u_1} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) (v : EuclideanSpace ℝ (Fin d)) : (S.centers ∩ (v +ᵥ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b))).encard = ↑S.numReps

noncomputable instance PeriodicSpherePacking.instFintypeNumReps' {d : ℕ} (S : PeriodicSpherePacking d) (hd : 0 < d) {D : Set (EuclideanSpace ℝ (Fin d))} (hD_isBounded : Bornology.IsBounded D) : Fintype ↑(S.centers ∩ D)

Equations

• S.instFintypeNumReps' hd hD_isBounded = Fintype.ofFinite ↑(S.centers ∩ D)

noncomputable def PeriodicSpherePacking.numReps' {d : ℕ} (S : PeriodicSpherePacking d) (hd : 0 < d) {D : Set (EuclideanSpace ℝ (Fin d))} (hD_isBounded : Bornology.IsBounded D) : ℕ

Equations

• S.numReps' hd hD_isBounded = Fintype.card ↑(S.centers ∩ D)

theorem PeriodicSpherePacking.numReps'_nonneg {d : ℕ} (S : PeriodicSpherePacking d) (hd : 0 < d) {D : Set (EuclideanSpace ℝ (Fin d))} (hD_isBounded : Bornology.IsBounded D) : 0 ≤ S.numReps' hd hD_isBounded

theorem PeriodicSpherePacking.numReps_eq_numReps' {d : ℕ} (S : PeriodicSpherePacking d) (hd : 0 < d) {D : Set (EuclideanSpace ℝ (Fin d))} (hD_isBounded : Bornology.IsBounded D) (hD_unique_covers : ∀ (x : EuclideanSpace ℝ (Fin d)), ∃! g : ↥S.lattice, g +ᵥ x ∈ D) : S.numReps = S.numReps' hd hD_isBounded

theorem PeriodicSpherePacking.aux_ge {d : ℕ} (S : PeriodicSpherePacking d) (hd : 0 < d) {ι : Type u_1} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) {L : ℝ} (hL : ∀ x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b), ‖x‖ ≤ L) (R : ℝ) : (S.centers ∩ Metric.ball 0 R).encard ≥ S.numReps • (↑S.lattice ∩ Metric.ball 0 (R - L)).encard

theorem PeriodicSpherePacking.aux_le {d : ℕ} (S : PeriodicSpherePacking d) (hd : 0 < d) {ι : Type u_1} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) {L : ℝ} (hL : ∀ x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b), ‖x‖ ≤ L) (R : ℝ) : (S.centers ∩ Metric.ball 0 R).encard ≤ S.numReps • (↑S.lattice ∩ Metric.ball 0 (R + L)).encard

theorem aux7 {d : ℕ} (S : PeriodicSpherePacking d) (D : Set (EuclideanSpace ℝ (Fin d))) {L : ℝ} (R : ℝ) (hD_unique_covers : ∀ (x : EuclideanSpace ℝ (Fin d)), ∃! g : ↥S.lattice, g +ᵥ x ∈ D) (hL : ∀ x ∈ D, ‖x‖ ≤ L) : Metric.ball 0 (R - L) ⊆ ⋃ x ∈ ↑S.lattice ∩ Metric.ball 0 R, x +ᵥ D

theorem PeriodicSpherePacking.aux2_ge {d : ℕ} (S : PeriodicSpherePacking d) (D : Set (EuclideanSpace ℝ (Fin d))) {L : ℝ} (R : ℝ) (hD_unique_covers : ∀ (x : EuclideanSpace ℝ (Fin d)), ∃! g : ↥S.lattice, g +ᵥ x ∈ D) (hD_measurable : MeasurableSet D) (hL : ∀ x ∈ D, ‖x‖ ≤ L) (hd : 0 < d) : ↑(↑S.lattice ∩ Metric.ball 0 R).encard ≥ MeasureTheory.volume (Metric.ball 0 (R - L)) / MeasureTheory.volume D

theorem aux8 {d : ℕ} (S : PeriodicSpherePacking d) (D : Set (EuclideanSpace ℝ (Fin d))) {L : ℝ} (R : ℝ) (hD_unique_covers : ∀ (x : EuclideanSpace ℝ (Fin d)), ∃! g : ↥S.lattice, g +ᵥ x ∈ D) (hL : ∀ x ∈ D, ‖x‖ ≤ L) : ⋃ x ∈ ↑S.lattice ∩ Metric.ball 0 R, x +ᵥ D ⊆ Metric.ball 0 (R + L)

theorem PeriodicSpherePacking.aux2_le {d : ℕ} (S : PeriodicSpherePacking d) (D : Set (EuclideanSpace ℝ (Fin d))) {L : ℝ} (R : ℝ) (hD_unique_covers : ∀ (x : EuclideanSpace ℝ (Fin d)), ∃! g : ↥S.lattice, g +ᵥ x ∈ D) (hD_measurable : MeasurableSet D) (hL : ∀ x ∈ D, ‖x‖ ≤ L) (hd : 0 < d) : ↑(↑S.lattice ∩ Metric.ball 0 R).encard ≤ MeasureTheory.volume (Metric.ball 0 (R + L)) / MeasureTheory.volume D

theorem PeriodicSpherePacking.aux2_ge' {d : ℕ} (S : PeriodicSpherePacking d) {ι : Type u_1} [Fintype ι] {L : ℝ} (R : ℝ) (b : Basis ι ℤ ↥S.lattice) (hL : ∀ x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b), ‖x‖ ≤ L) (hd : 0 < d) : ↑(↑S.lattice ∩ Metric.ball 0 R).encard ≥ MeasureTheory.volume (Metric.ball 0 (R - L)) / MeasureTheory.volume (ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b))

theorem PeriodicSpherePacking.aux2_le' {d : ℕ} (S : PeriodicSpherePacking d) {ι : Type u_1} [Fintype ι] {L : ℝ} (R : ℝ) (b : Basis ι ℤ ↥S.lattice) (hL : ∀ x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b), ‖x‖ ≤ L) (hd : 0 < d) : ↑(↑S.lattice ∩ Metric.ball 0 R).encard ≤ MeasureTheory.volume (Metric.ball 0 (R + L)) / MeasureTheory.volume (ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b))

theorem aux_big_le {d : ℕ} {S : PeriodicSpherePacking d} {ι : Type u_2} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) {L : ℝ} (R : ℝ) (hL : ∀ x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b), ‖x‖ ≤ L) (hd : 0 < d) : S.finiteDensity R ≤ ↑S.numReps * MeasureTheory.volume (Metric.ball 0 (S.separation / 2)) / MeasureTheory.volume (ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b)) * (MeasureTheory.volume (Metric.ball 0 (R + S.separation / 2 + L * 2)) / MeasureTheory.volume (Metric.ball 0 R))

theorem aux_big_ge {d : ℕ} {S : PeriodicSpherePacking d} {ι : Type u_2} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) {L : ℝ} (R : ℝ) (hL : ∀ x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b), ‖x‖ ≤ L) (hd : 0 < d) : S.finiteDensity R ≥ ↑S.numReps * MeasureTheory.volume (Metric.ball 0 (S.separation / 2)) / MeasureTheory.volume (ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b)) * (MeasureTheory.volume (Metric.ball 0 (R - S.separation / 2 - L * 2)) / MeasureTheory.volume (Metric.ball 0 R))

theorem volume_ball_ratio_tendsto_nhds_one {d : ℕ} {C : ℝ} (hd : 0 < d) (hC : 0 ≤ C) : Filter.Tendsto (fun (R : ℝ) => MeasureTheory.volume (Metric.ball 0 R) / MeasureTheory.volume (Metric.ball 0 (R + C))) Filter.atTop (nhds 1)

theorem volume_ball_ratio_tendsto_nhds_one' {d : ℕ} {C C' : ℝ} (hd : 0 < d) (hC : 0 ≤ C) (hC' : 0 ≤ C') : Filter.Tendsto (fun (R : ℝ) => MeasureTheory.volume (Metric.ball 0 (R + C)) / MeasureTheory.volume (Metric.ball 0 (R + C'))) Filter.atTop (nhds 1)

theorem Filter.map_add_atTop_eq {β : Type u_3} {f : ℝ → β} (C : ℝ) (α : Filter β) : Tendsto f atTop α ↔ Tendsto (fun (x : ℝ) => f (x + C)) atTop α

theorem volume_ball_ratio_tendsto_nhds_one'' {d : ℕ} {C C' : ℝ} (hd : 0 < d) : Filter.Tendsto (fun (R : ℝ) => MeasureTheory.volume (Metric.ball 0 (R + C)) / MeasureTheory.volume (Metric.ball 0 (R + C'))) Filter.atTop (nhds 1)

theorem PeriodicSpherePacking.density_eq {d : ℕ} {S : PeriodicSpherePacking d} {ι : Type u_3} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) {L : ℝ} (hL : ∀ x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b), ‖x‖ ≤ L) (hd : 0 < d) : S.density = ↑S.numReps * MeasureTheory.volume (Metric.ball 0 (S.separation / 2)) / MeasureTheory.volume (ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b))

theorem periodic_constant_eq_periodic_constant_normalized {d : ℕ} (hd : 0 < d) : PeriodicSpherePackingConstant d = ⨆ (S : PeriodicSpherePacking d), ⨆ (_ : S.separation = 1), S.density

theorem PeriodicSpherePacking.unique_covers_of_centers {d : ℕ} (S : PeriodicSpherePacking d) {D : Set (EuclideanSpace ℝ (Fin d))} (hD_unique_covers : ∀ (x : EuclideanSpace ℝ (Fin d)), ∃! g : ↥S.lattice, g +ᵥ x ∈ D) (x : ↑S.centers) : ∃! g : ↥S.lattice, ↑(g +ᵥ x) ∈ S.centers ∩ D

theorem PeriodicSpherePacking.centers_union_over_lattice {d : ℕ} (S : PeriodicSpherePacking d) {D : Set (EuclideanSpace ℝ (Fin d))} (hD_unique_covers : ∀ (x : EuclideanSpace ℝ (Fin d)), ∃! g : ↥S.lattice, g +ᵥ x ∈ D) : S.centers = ⋃ (g : ↥S.lattice), g +ᵥ S.centers ∩ D

theorem PeriodicSpherePacking.exists_bound_on_fundamental_domain {d : ℕ} (S : PeriodicSpherePacking d) (b : Basis (Fin d) ℤ ↥S.lattice) : ∃ (L : ℝ), ∀ x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b), ‖x‖ ≤ L

theorem PeriodicSpherePacking.fundamental_domain_unique_covers {d : ℕ} (S : PeriodicSpherePacking d) (b : Basis (Fin d) ℤ ↥S.lattice) (x : EuclideanSpace ℝ (Fin d)) : ∃! g : ↥S.lattice, g +ᵥ x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ S.lattice b)

noncomputable instance HDivENNReal : HDiv NNReal ENNReal ENNReal

Equations

• HDivENNReal = { hDiv := fun (x : NNReal) (y : ENNReal) => ↑x / y }

noncomputable instance HMulENNReal : HMul NNReal ENNReal ENNReal

Equations

• HMulENNReal = { hMul := fun (x : NNReal) (y : ENNReal) => ↑x * y }

noncomputable def ZLattice.basis_index_equiv {d : ℕ} (Λ : Submodule ℤ (EuclideanSpace ℝ (Fin d))) [DiscreteTopology ↥Λ] [IsZLattice ℝ Λ] : Module.Free.ChooseBasisIndex ℤ ↥Λ ≃ Fin d

Equations

• ZLattice.basis_index_equiv Λ = Fintype.equivFinOfCardEq ⋯

noncomputable def PeriodicSpherePacking.basis_index_equiv {d : ℕ} (P : PeriodicSpherePacking d) : Module.Free.ChooseBasisIndex ℤ ↥P.lattice ≃ Fin d

Equations

• P.basis_index_equiv = ZLattice.basis_index_equiv P.lattice

@[simp]

theorem PeriodicSpherePacking.density_eq' {d : ℕ} (S : PeriodicSpherePacking d) (hd : 0 < d) : S.density = ↑↑S.numReps * MeasureTheory.volume (Metric.ball 0 (S.separation / 2)) / ↑(ZLattice.covolume S.lattice MeasureTheory.volume).toNNReal

theorem PeriodicSpherePacking.density_of_centers_empty {d : ℕ} (S : PeriodicSpherePacking d) (hd : 0 < d) [instEmpty : IsEmpty ↑S.centers] : S.density = 0

theorem SpherePacking.density_of_centers_empty {d : ℕ} (S : SpherePacking d) (hd : 0 < d) [instEmpty : IsEmpty ↑S.centers] : S.density = 0

theorem periodic_constant_eq_constant {d : ℕ} (hd : 0 < d) : PeriodicSpherePackingConstant d = SpherePackingConstant d