module
module
IndisputableMonolith.Constants.GapWeight.Projection
show as:
view Lean formalization →
used by (1)
depends on (3)
declarations in this module (17)
-
def
N_ticks -
theorem
N_ticks_eq -
def
N_vertices -
theorem
N_vertices_eq -
def
N_cell -
theorem
N_cell_eq -
def
projectionScale -
theorem
projectionScale_eq -
def
phiDFTEnergyTotal -
lemma
phiDFTEnergyTotal_nonneg -
def
w8_projected -
lemma
w8_projected_nonneg -
def
diff8 -
def
diffEnergy8 -
lemma
diffEnergy8_nonneg -
lemma
dft8_mode_normSq_sum -
lemma
diffEnergy8_mode