diff --git a/web/dependencies/commuting_hermitian/index.html b/web/dependencies/commuting_hermitian/index.html new file mode 100644 --- /dev/null +++ b/web/dependencies/commuting_hermitian/index.html @@ -0,0 +1,92 @@ + + + + + + Commuting_Hermitian - Archive of Formal Proofs + + + + + + + + + + + + + + + + + + + + + + + + +
+
+
+ + + +
+
+

+ Commuting_Hermitian Dependents

+
+ + +
+

2023

+ + + + +
+
+ + + \ No newline at end of file diff --git a/web/dependencies/commuting_hermitian/index.xml b/web/dependencies/commuting_hermitian/index.xml new file mode 100644 --- /dev/null +++ b/web/dependencies/commuting_hermitian/index.xml @@ -0,0 +1,20 @@ + + + + Commuting_Hermitian on Archive of Formal Proofs + /dependencies/commuting_hermitian/ + Recent content in Commuting_Hermitian on Archive of Formal Proofs + Hugo -- gohugo.io + en-gb + Fri, 03 Mar 2023 00:00:00 +0000 + + Expander Graphs + /entries/Expander_Graphs.html + Fri, 03 Mar 2023 00:00:00 +0000 + + /entries/Expander_Graphs.html + + + + + diff --git a/web/dependencies/frequency_moments/index.html b/web/dependencies/frequency_moments/index.html new file mode 100644 --- /dev/null +++ b/web/dependencies/frequency_moments/index.html @@ -0,0 +1,92 @@ + + + + + + Frequency_Moments - Archive of Formal Proofs + + + + + + + + + + + + + + + + + + + + + + + + +
+
+
+ + + +
+
+

+ Frequency_Moments Dependents

+
+ + +
+

2023

+ + + + +
+
+ + + \ No newline at end of file diff --git a/web/dependencies/frequency_moments/index.xml b/web/dependencies/frequency_moments/index.xml new file mode 100644 --- /dev/null +++ b/web/dependencies/frequency_moments/index.xml @@ -0,0 +1,20 @@ + + + + Frequency_Moments on Archive of Formal Proofs + /dependencies/frequency_moments/ + Recent content in Frequency_Moments on Archive of Formal Proofs + Hugo -- gohugo.io + en-gb + Fri, 03 Mar 2023 00:00:00 +0000 + + Expander Graphs + /entries/Expander_Graphs.html + Fri, 03 Mar 2023 00:00:00 +0000 + + /entries/Expander_Graphs.html + + + + + diff --git a/web/dependencies/weighted_arithmetic_geometric_mean/index.html b/web/dependencies/weighted_arithmetic_geometric_mean/index.html new file mode 100644 --- /dev/null +++ b/web/dependencies/weighted_arithmetic_geometric_mean/index.html @@ -0,0 +1,92 @@ + + + + + + Weighted_Arithmetic_Geometric_Mean - Archive of Formal Proofs + + + + + + + + + + + + + + + + + + + + + + + + +
+
+
+ + + +
+
+

+ Weighted_Arithmetic_Geometric_Mean Dependents

+
+ + +
+

2023

+ + + + +
+
+ + + \ No newline at end of file diff --git a/web/dependencies/weighted_arithmetic_geometric_mean/index.xml b/web/dependencies/weighted_arithmetic_geometric_mean/index.xml new file mode 100644 --- /dev/null +++ b/web/dependencies/weighted_arithmetic_geometric_mean/index.xml @@ -0,0 +1,20 @@ + + + + Weighted_Arithmetic_Geometric_Mean on Archive of Formal Proofs + /dependencies/weighted_arithmetic_geometric_mean/ + Recent content in Weighted_Arithmetic_Geometric_Mean on Archive of Formal Proofs + Hugo -- gohugo.io + en-gb + Fri, 03 Mar 2023 00:00:00 +0000 + + Expander Graphs + /entries/Expander_Graphs.html + Fri, 03 Mar 2023 00:00:00 +0000 + + /entries/Expander_Graphs.html + + + + + diff --git a/web/entries/Expander_Graphs.html b/web/entries/Expander_Graphs.html new file mode 100644 --- /dev/null +++ b/web/entries/Expander_Graphs.html @@ -0,0 +1,177 @@ + + + + + + Expander Graphs - Archive of Formal Proofs + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+
+
+ + + +
+
+

+ Expander Graphs

+
+ +

Emin Karayel 📧 +

+ + +

March 3, 2023

+ +
+

Abstract

+ +
Expander Graphs are low-degree graphs that are highly connected. They have diverse +applications, for example in derandomization and pseudo-randomness, error-correcting codes, as well +as pure mathematical subjects such as metric embeddings. This entry formalizes the concept and +derives main theorems about them such as Cheeger's inequality or tail bounds on distribution of +random walks on them. It includes a strongly explicit construction for every size and spectral gap. +The latter is based on the Margulis-Gabber-Galil graphs and several graph operations +that preserve spectral properties. The proofs are based on the survey papers/monographs +by Hoory et al. and Vadhan, as well as results from Impagliazzo and Kabanets and Murtagh et al.
+ +

License

+
BSD License

Topics

+ +

Session Expander_Graphs

+ +
+ + + +
+ + +
+ +
+ + +
+
+
+ + + \ No newline at end of file diff --git a/web/theories/expander_graphs/index.html b/web/theories/expander_graphs/index.html new file mode 100644 --- /dev/null +++ b/web/theories/expander_graphs/index.html @@ -0,0 +1,94 @@ + + + + + + Expander_Graphs - Archive of Formal Proofs + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+
+
+ + + +
+
+

+ Expander_Graphs

+
+ + +
+
+

Constructive_Chernoff_Bound

+

Extra_Congruence_Method

+

Expander_Graphs_Multiset_Extras

+

Expander_Graphs_Definition

+

Expander_Graphs_TTS

+

Expander_Graphs_Algebra

+

Expander_Graphs_Eigenvalues

+

Expander_Graphs_Cheeger_Inequality

+

Expander_Graphs_MGG

+

Expander_Graphs_Walks

+

Expander_Graphs_Power_Construction

+

Expander_Graphs_Strongly_Explicit

+
+
+ + + \ No newline at end of file