ConvectionOp — Recognition explainer

formal statement (Lean)

  77def ConvectionOp (N : ℕ) : Type :=

proof body

Definition body.

  78  GalerkinState N → GalerkinState N → GalerkinState N
  79
  80/-- Discrete Navier–Stokes RHS: u' = νΔu - B(u,u). -/

used by (26)

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

aestronglyMeasurable_galerkinForcing_mode_of_continuous in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
duhamelRemainderOfGalerkin_integratingFactor in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
duhamelRemainderOfGalerkin_kernel in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
forcingDCTAt in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
galerkin_duhamelKernel_identity in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
galerkinForcing in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
GalerkinForcingDominatedConvergenceHypothesis in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
galerkinNS_hasDerivAt_duhamelRemainder_mode in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
galerkinNS_hasDerivAt_extendByZero_mode in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
nsDuhamelCoeffBound_galerkinKernel 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
of_convectionNormBound_of_continuous in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
UniformBoundsHypothesis in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
EnergySkewHypothesis in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
galerkinNSRHS in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
inviscid_energy_deriv_zero in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
viscous_energy_antitone in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
viscous_energy_bound_from_initial in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
viscous_energy_deriv_le_zero in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
viscous_energy_deriv_nonpos in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
viscous_norm_bound_from_initial in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel in IndisputableMonolith.ClassicalBridge.Fluids.Regularity2D decl_use
rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcing in IndisputableMonolith.ClassicalBridge.Fluids.Regularity2D decl_use
rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp in IndisputableMonolith.ClassicalBridge.Fluids.Regularity2D decl_use

depends on (1)

Lean names referenced from this declaration's body.

GalerkinState in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use