def definition def or abbrev

`trajectory`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  91def trajectory (f : ℝ → ℝ) (r : ℝ) : ℕ → ℝ
  92  | 0 => r
  93  | n + 1 => f (trajectory f r n)
  94

used by (40)

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

applied in IndisputableMonolith.Action.EnergyConservationDomainCert decl_use
costRateEL_implies_const_one in IndisputableMonolith.Action.EulerLagrange decl_use
hamilton_equations_from_EL in IndisputableMonolith.Action.Hamiltonian decl_use
hamiltonPDotEquation in IndisputableMonolith.Action.Hamiltonian decl_use
totalEnergy in IndisputableMonolith.Action.Hamiltonian decl_use
spaceShift in IndisputableMonolith.Action.Noether decl_use
standardLagrangian in IndisputableMonolith.Action.QuadraticLimit decl_use
duhamelRemainderOfGalerkin in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
duhamelRemainderOfGalerkin_kernel in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
forcingDCTAt in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
galerkinNS_hasDerivAt_extendByZero_mode in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
IdentificationHypothesis in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
IsDivergenceFree in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
IsStokesMildTraj in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
nsDuhamel_of_forall in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
nsDuhamel_of_forall_kernelIntegral_of_forcing in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
of_convectionNormBound_of_continuous in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
stokesODE in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
RSNS2DPipelineHypothesis in IndisputableMonolith.ClassicalBridge.Fluids.Regularity2D decl_use
BaryogenesisTrajectoryCert in IndisputableMonolith.Cosmology.BaryogenesisTrajectory decl_use
etaB_at_gap45 in IndisputableMonolith.Cosmology.BaryogenesisTrajectoryFromPhiLadder decl_use
V_pos_off_vacuum in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost decl_use
octavePhase in IndisputableMonolith.Cost.Ndim.Octave decl_use
conservation_is_unconditional in IndisputableMonolith.Foundation.TopologicalConservation decl_use
negCharge in IndisputableMonolith.Foundation.TopologicalConservation decl_use
Trajectory in IndisputableMonolith.Foundation.VariationalDynamics decl_use
unity_is_equilibrium in IndisputableMonolith.Foundation.VariationalDynamics decl_use
variational_dynamics_deterministic in IndisputableMonolith.Foundation.VariationalDynamics decl_use
variational_step_reduces_defect in IndisputableMonolith.Foundation.VariationalDynamics decl_use
fib_10_eq in IndisputableMonolith.Gravity.JCostInflaton decl_use

… and 10 more