modes — Recognition explainer

formal statement (Lean)

  41noncomputable def modes (N : ℕ) : Finset Mode2 :=

proof body

Definition body.

  42  ((Finset.Icc (-((N : ℤ))) (N : ℤ)).product (Finset.Icc (-((N : ℤ))) (N : ℤ)))
  43

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

Jphi_numerical_band in IndisputableMonolith.Aesthetics.VisualBeauty decl_use
lambda_PBM_approx in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
phi_eighth_in_gamma_band in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
coeffAt in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
coeffAt_add in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
coeffAt_smul in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
extendByZero_laplacianCoeff in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
FourierState2D in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
galerkinForcing in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
GalerkinForcingDominatedConvergenceHypothesis in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
norm_extendByZero_le in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
nsDuhamelCoeffBound_galerkinKernel_of_forcing in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
of_convectionNormBound in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
GalerkinState in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
laplacianCoeff_inner_self_nonpos in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
mem_modes_iff in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
modeTrunc in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
encodeGalerkin2D in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics decl_use
encodeIndex in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics decl_use
coeffMag_foldPlusOneStep in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
coeffSign_foldPlusOneStep in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
decide_lt_zero_foldPlusOneStep in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
decodeCoeff_voxelStep_foldMinusOne_encodeIndex in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
decodeGalerkin2D in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
foldMinusOneDecodedStep in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
foldPlusOneStep in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
SimulationHypothesis in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
voxelStep_foldPlusOne_encodeIndex in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
equation_of_state in IndisputableMonolith.Cosmology.DarkEnergyEOS decl_use

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.

Mode2 in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use