def definition def or abbrev

`TailFluxVanish`

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

formal statement (Lean)

  36def TailFluxVanish (A A' : ℝ → ℝ) : Prop :=

proof body

Definition body.

  37  Tendsto (fun r : ℝ => tailFlux A A' r) atTop (𝓝 0)
  38
  39/-- Abstract profile for a fixed time-slice RM2U coefficient, with derivative data. -/

used by (21)

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

bet2_for_galerkin in IndisputableMonolith.NavierStokes.RM2U.BetInstantiation decl_use
BetInstantiationCert in IndisputableMonolith.NavierStokes.RM2U.BetInstantiation decl_use
nonParasitism_for_galerkin in IndisputableMonolith.NavierStokes.RM2U.BetInstantiation decl_use
rm2u_pipeline_complete in IndisputableMonolith.NavierStokes.RM2U.BetInstantiation decl_use
tailFlux_vanishes_for_galerkin in IndisputableMonolith.NavierStokes.RM2U.BetInstantiation decl_use
boundaryTerm in IndisputableMonolith.NavierStokes.RM2U.Core decl_use
tailFluxVanish in IndisputableMonolith.NavierStokes.RM2U.Core decl_use
coerciveL2Bound_of_tailFluxVanish in IndisputableMonolith.NavierStokes.RM2U.EnergyIdentity decl_use
TailFluxVanishImpliesCoerciveHypothesis in IndisputableMonolith.NavierStokes.RM2U.EnergyIdentity decl_use
tailFluxVanish_of_integrable in IndisputableMonolith.NavierStokes.RM2U.EnergyIdentity decl_use
Bet2SelfFalsificationHypothesis in IndisputableMonolith.NavierStokes.RM2U.NonParasitism decl_use
NonParasitismHypothesis in IndisputableMonolith.NavierStokes.RM2U.NonParasitism decl_use
of_u4 in IndisputableMonolith.NavierStokes.RM2U.NonParasitism decl_use
PrimeScheduleSelfFalsification in IndisputableMonolith.NavierStokes.RM2U.NonParasitism decl_use
TailFluxNonVanishImpliesExportAtSmallScales in IndisputableMonolith.NavierStokes.RM2U.NonParasitism decl_use
ancientDecay_implies_coercive in IndisputableMonolith.NavierStokes.RM2U.TailFluxInstantiation decl_use
ancientDecay_implies_tailFlux_vanish in IndisputableMonolith.NavierStokes.RM2U.TailFluxInstantiation decl_use
EnergyForcingHypothesis in IndisputableMonolith.NavierStokes.RM2U.TailFluxInstantiation decl_use
sobolev_H1_half_line_decay in IndisputableMonolith.NavierStokes.RM2U.TailFluxInstantiation decl_use
TailFluxInstantiationCert in IndisputableMonolith.NavierStokes.RM2U.TailFluxInstantiation decl_use
tailFlux_vanishes_from_weighted_moment in IndisputableMonolith.NavierStokes.RM2U.TailFluxInstantiation decl_use

depends on (5)

Lean names referenced from this declaration's body.

A in IndisputableMonolith.Foundation.IntegrationGap decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
tailFlux in IndisputableMonolith.NavierStokes.RM2U.Core decl_use