structure definition def or abbrev

`Strategy`

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

formal statement (Lean)

  40structure Strategy where
  41  apply : {n : ℕ} → (Fin n → ℝ) → (Fin n → ℝ)
  42
  43/-- Sigma spread after applying a strategy. -/

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

all_ml_on_phi_ladder in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
tau0_planck_relation in IndisputableMonolith.Constants.Derivation decl_use
representation_formula in IndisputableMonolith.Cost.AczelProof decl_use
loveStrategy in IndisputableMonolith.Ethics.SigmaEquilibrationAsDrive decl_use
selfishStrategy in IndisputableMonolith.Ethics.SigmaEquilibrationAsDrive decl_use
spreadAfter in IndisputableMonolith.Ethics.SigmaEquilibrationAsDrive decl_use
flow_contribution_reciprocal in IndisputableMonolith.Foundation.LedgerForcing decl_use
rescaleLength_tendsto_zero in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use
logPhiInterval in IndisputableMonolith.Numerics.Interval.Log decl_use
phi_neg58_lt in IndisputableMonolith.Numerics.Interval.PhiBounds decl_use
spatialRadius_coordRay_ne_zero_proved in IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs decl_use
riemann_lowered_antisym_first in IndisputableMonolith.Relativity.Geometry.RiemannSymmetries decl_use
coupling_product_small_proven in IndisputableMonolith.Relativity.GRLimit.Parameters decl_use
bose_can_exceed_one in IndisputableMonolith.Thermodynamics.BoseEinstein decl_use