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)
14structure DisplayChannel (State Obs : Type*) where
15 observe : State → Obs
16 quality : Obs → ℝ
17
18namespace DisplayChannel
19
20variable {State Obs : Type*}
21
22/-- The composed quality function: State → ℝ. -/
used by (12)
From the project-wide theorem graph. These declarations reference this one in their body.
-
ChannelBundle
in IndisputableMonolith.RRF.Core.DisplayChannel
decl_use
-
isOptimal
in IndisputableMonolith.RRF.Core.DisplayChannel
decl_use
-
optimal_iff
in IndisputableMonolith.RRF.Core.DisplayChannel
decl_use
-
QualityEquiv
in IndisputableMonolith.RRF.Core.DisplayChannel
decl_use
-
refl
in IndisputableMonolith.RRF.Core.DisplayChannel
decl_use
-
stateQuality
in IndisputableMonolith.RRF.Core.DisplayChannel
decl_use
-
symm
in IndisputableMonolith.RRF.Core.DisplayChannel
decl_use
-
trans
in IndisputableMonolith.RRF.Core.DisplayChannel
decl_use
-
quadratic1DChannel
in IndisputableMonolith.RRF.Models.Quadratic
decl_use
-
trivialChannel
in IndisputableMonolith.RRF.Models.Trivial
decl_use
-
channel_mono_transfer
in IndisputableMonolith.RRF.Theorems.OrderPreservation
decl_use
-
optimal_transfer
in IndisputableMonolith.RRF.Theorems.OrderPreservation
decl_use
depends on (2)
Lean names referenced from this declaration's body.
-
State
in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D
decl_use
-
State
in IndisputableMonolith.NavierStokes.DiscreteVorticity
decl_use