Documentation

LeanPool.ParameterFreeGradient.V7.Proofs.Stage6StrictDeterministic.HSelection

Selection of a hard-family scale beyond every query and output in a finite transcript.

def V7.Stage6StrictDeterministic.traceDisplacementBound (x0 : StrictPoint) :

StrictTranscript → ℝ

Oriented finite displacement maximum, with zero included explicitly.

Equations

V7.Stage6StrictDeterministic.traceDisplacementBound x0 [] = 0
V7.Stage6StrictDeterministic.traceDisplacementBound x0 (obs :: trace) = max (obs.point 0 - x0 0) (V7.Stage6StrictDeterministic.traceDisplacementBound x0 trace)

Instances For

@[simp]

theorem V7.Stage6StrictDeterministic.traceDisplacementBound_nil (x0 : StrictPoint) :

traceDisplacementBound x0 [] = 0

@[simp]

theorem V7.Stage6StrictDeterministic.traceDisplacementBound_cons (x0 : StrictPoint) (obs : StrictObservation) (trace : StrictTranscript) :

traceDisplacementBound x0 (obs :: trace) = max (obs.point 0 - x0 0) (traceDisplacementBound x0 trace)

theorem V7.Stage6StrictDeterministic.traceDisplacementBound_nonneg (x0 : StrictPoint) (trace : StrictTranscript) :

0 ≤ traceDisplacementBound x0 trace

theorem V7.Stage6StrictDeterministic.displacement_le_traceDisplacementBound (x0 : StrictPoint) {trace : StrictTranscript} {obs : StrictObservation} (hobs : obs ∈ trace) :

obs.point 0 - x0 0 ≤ traceDisplacementBound x0 trace

def V7.Stage6StrictDeterministic.postTranscriptH (method : StrictLocalMethod) (N : ℕ) (trace : StrictTranscript) :

The transition is selected only after the complete trace and finite output are fixed. Adding one makes all frozen oriented bounds strict.

Equations

V7.Stage6StrictDeterministic.postTranscriptH method N trace = max (V7.Stage6StrictDeterministic.traceDisplacementBound method.x0 trace) (method.output N trace 0 - method.x0 0) + 1

Instances For

theorem V7.Stage6StrictDeterministic.postTranscriptH_pos (method : StrictLocalMethod) (N : ℕ) (trace : StrictTranscript) :

0 < postTranscriptH method N trace

theorem V7.Stage6StrictDeterministic.trace_displacement_lt_postTranscriptH (method : StrictLocalMethod) (N : ℕ) (trace : StrictTranscript) (obs : StrictObservation) :

obs ∈ trace → obs.point 0 - method.x0 0 < postTranscriptH method N trace

theorem V7.Stage6StrictDeterministic.output_displacement_lt_postTranscriptH (method : StrictLocalMethod) (N : ℕ) (trace : StrictTranscript) :

method.output N trace 0 - method.x0 0 < postTranscriptH method N trace