Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section5.RelativeError.TraceInstanceInterface

The positive-word trace interface shared by the producer and step-down estimate consumers #

source
def AVenhance.Infra.Section5.RelativeError.e44PositiveTraceInput (β : ℝ) (I : Ingredients β) (κ : ℝ) (M m : ℕ) (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (Ctr : ℝ) :
Prop

Literal trace formula, stated independently of the profile consumer module so the Fourier construction and its adapters can be built in separate import components. It unfolds to T1hThetaInitialTraceInput.

Equations
  • One or more equations did not get rendered due to their size.
Instances For