def definition def or abbrev

`sampleW`

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

formal statement (Lean)

 159def sampleW : PatternLayer.Pattern 8 := fun i => decide (i.1 % 2 = 0)

proof body

Definition body.

 160
 161-- Example checks (can be evaluated in an interactive session)
 162-- #eval PatternLayer.Z_of_window sampleW
 163-- #eval MeasurementLayer.observeAvg8 3 (PatternLayer.extendPeriodic8 sampleW)
 164
 165end Examples
 166
 167end IndisputableMonolith

depends on (14)

Lean names referenced from this declaration's body.

eval in IndisputableMonolith.Foundation.LogicAsFunctionalEquation.LinearLogicBridge decl_use
extendPeriodic8 in IndisputableMonolith.Measurement decl_use
observeAvg8 in IndisputableMonolith.Measurement decl_use
Pattern in IndisputableMonolith.Measurement decl_use
Z_of_window in IndisputableMonolith.Measurement decl_use
Pattern in IndisputableMonolith.Patterns decl_use
eval in IndisputableMonolith.Relativity.Fields.Scalar decl_use
extendPeriodic8 in IndisputableMonolith.Streams decl_use
Pattern in IndisputableMonolith.Streams decl_use
Z_of_window in IndisputableMonolith.Streams decl_use
extendPeriodic8 in IndisputableMonolith.Streams.Blocks decl_use
observeAvg8 in IndisputableMonolith.Streams.Blocks decl_use
Pattern in IndisputableMonolith.Streams.Blocks decl_use
Z_of_window in IndisputableMonolith.Streams.Blocks decl_use