No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
69structure Map (State Obs : Type) where
70 T : ℝ
71 T_pos : 0 < T
72 meas : (ℝ → State) → ℝ → Obs
73
74/-- Midpoint sampling average (lightweight helper). -/
used by (14)
From the project-wide theorem graph. These declarations reference this one in their body.
-
SuperconductorFamily
in IndisputableMonolith.Chemistry.SuperconductingTc
decl_use
-
ClayBridge
in IndisputableMonolith.Complexity.ComputationBridge
decl_use
-
mul
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
-
mul
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
-
torsion8
in IndisputableMonolith.Masses.Ribbons
decl_use
-
MockThetaPhantomCorrespondence
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
map
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
Measurement
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
canonicalAnchor
in IndisputableMonolith.Physics.AnchorPolicy
decl_use
-
quotientMk_respects_event
in IndisputableMonolith.RecogGeom.Quotient
decl_use
-
apply
in IndisputableMonolith.RecogSpec.Scales
decl_use
-
Bands
in IndisputableMonolith.Relativity.ILG.Action
decl_use
-
VantageFunctor
in IndisputableMonolith.RRF.Foundation.VantageCategory
decl_use
-
apply
in IndisputableMonolith.UnitMapping
decl_use
depends on (4)
Lean names referenced from this declaration's body.
-
State
in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D
decl_use
-
T
in IndisputableMonolith.Foundation.Breath1024
decl_use
-
T
in IndisputableMonolith.Gap45.SyncMinimization
decl_use
-
State
in IndisputableMonolith.NavierStokes.DiscreteVorticity
decl_use