Source indexedlemma · leanprover/lean4:v4.32.0

enumΘ'ArgMax_eq_iff

Carleson.MetricCarleson.Main · Carleson/MetricCarleson/Main.lean:110 to 118

Source documentation

The characterising property of enumΘ'ArgMax.

Exact Lean statement

lemma enumΘ'ArgMax_eq_iff {n i : ℕ} {x : X} (hi : i ≤ n) :
    enumΘ'ArgMax nΘ' g n x = i ↔
    (∀ j ≤ n, g (enumΘ' nΘ' j) x ≤ g (enumΘ' nΘ' i) x) ∧
    ∀ j < i, g (enumΘ' nΘ' j) x < g (enumΘ' nΘ' i) x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma enumΘ'ArgMax_eq_iff {n i : ℕ} {x : X} (hi : i ≤ n) :    enumΘ'ArgMax nΘ' g n x = i ↔    (∀ j ≤ n, g (enumΘ' nΘ' j) x ≤ g (enumΘ' nΘ' i) x) ∧    ∀ j < i, g (enumΘ' nΘ' j) x < g (enumΘ' nΘ' i) x := by  rw [enumΘ'ArgMax, List.findIdx_eq (by rw [List.length_range]; lia)]  simp_rw [List.getElem_range, decide_eq_true_eq, decide_eq_false_iff_not, not_forall, not_le,    exists_prop, and_congr_right_iff]  refine fun ismax ↦ forall₂_congr fun j lj ↦ ⟨fun h ↦ ?_, fun h ↦ by use i⟩  obtain ⟨k, lk, lk'⟩ := h; exact lk'.trans_le (ismax _ lk)