def definition def or abbrev

`MollifierCkRoute`

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

formal statement (Lean)

 247def MollifierCkRoute : Prop :=

proof body

Definition body.

 248  ∃ (φ : ℕ → ContDiffBump (0 : ℝ)),
 249    Filter.Tendsto (fun n => (φ n).rOut) Filter.atTop (nhds 0)
 250
 251set_option maxHeartbeats 400000 in
 252/-- Existence of a shrinking-support bump family on `ℝ`. -/

used by (2)

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

mollified_pointwise_tendsto in IndisputableMonolith.Foundation.GeneralizedDAlembert decl_use
mollifierCkRoute_exists in IndisputableMonolith.Foundation.GeneralizedDAlembert decl_use

depends on (5)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use