Literal restatements of the big-bound estimate / step-down part (i) statement bodies

BigBoundStatement β C₀ is the proposition of the public statement AVenhance.bigbound (Section4/BigBound.lean), and IndyStepDownPartIStatement β C₀ is the Step-down estimate AVenhance.indystepdown (Section4/IndyStepDown.lean) with its conclusion restricted to conjunct (i) (e.homogenization.m); conjunct (ii) is not stated here. The statement modules themselves may not be imported; the proof body can be replaced by exact <wiring theorem> …, which checks the restatement by definitional unfolding.

def AVenhance.Infra.Section5.Integration.BigBoundStatement (β C₀ : ℝ) : Prop

The proposition of the big-bound estimate AVenhance.bigbound β C₀ (restated).

Equations

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

def AVenhance.Infra.Section5.Integration.IndyStepDownPartIStatement (β C₀ : ℝ) : Prop

The step-down estimate AVenhance.indystepdown β C₀ with the conclusion cut down to conjunct (i) (e.homogenization.m); premises as in the statement.

Equations

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

def AVenhance.Infra.Section5.Integration.IndyStepDownStatement (β C₀ : ℝ) : Prop

The proposition of the step-down AVenhance.indystepdown β C₀ (conjunct (ii) gated by 6/5 ≤ β and the later scale condition), restated. Used as an explicit, distinctly named hypothesis by the main-theorem assembly; the statement file itself is never imported.

Equations

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