def RegularizedNewton.acceptingParameters {X : Type u} (f : X → ℝ) (stepMap : ℝ → X → X) (modelValue : ℝ → X → ℝ) (x : X) : Set ℝ

The core acceptance set at a current point x: a parameter M belongs to acceptingParameters f stepMap modelValue x exactly when the trial point T_M(x) satisfies the acceptance inequality f (T_M(x)) ≤ \tilde f_M(x).

@[simp]

theorem RegularizedNewton.mem_acceptingParameters_iff {X : Type u} (f : X → ℝ) (stepMap : ℝ → X → X) (modelValue : ℝ → X → ℝ) (x : X) (M : ℝ) : M ∈ acceptingParameters f stepMap modelValue x ↔ f (stepMap M x) ≤ modelValue M x

Membership in acceptingParameters is exactly the regularized-Newton acceptance inequality at the current point.

def RegularizedNewton.acceptedParameters {X : Type u} (f : X → ℝ) (stepMap : ℝ → X → X) (modelValue : ℝ → X → ℝ) (L0 L : ℝ) (x : X) : Set ℝ

Definition 4.1.16: the accepted regularized-Newton parameters at x are the admissible parameters M ∈ [L₀, 2L] that satisfy the acceptance inequality f (T_M(x)) ≤ \tilde f_M(x).

@[simp]

theorem RegularizedNewton.mem_acceptedParameters_iff {X : Type u} (f : X → ℝ) (stepMap : ℝ → X → X) (modelValue : ℝ → X → ℝ) (L0 L : ℝ) (x : X) (M : ℝ) : M ∈ acceptedParameters f stepMap modelValue L0 L x ↔ M ∈ Set.Icc L0 (2 * L) ∧ f (stepMap M x) ≤ modelValue M x

Membership in acceptedParameters recovers the textbook interval condition together with the acceptance inequality.

theorem RegularizedNewton.mem_acceptedParameters_of_mem_Icc_of_le_modelValue {X : Type u} {f : X → ℝ} {stepMap : ℝ → X → X} {modelValue : ℝ → X → ℝ} {L0 L : ℝ} (x : X) (M : ℝ) (hMmem : M ∈ Set.Icc L0 (2 * L)) (haccept : f (stepMap M x) ≤ modelValue M x) : M ∈ acceptedParameters f stepMap modelValue L0 L x

An admissible parameter belongs to acceptedParameters as soon as it satisfies the regularized-Newton acceptance inequality at the same current point.