Mathoverflow 347178

Reference: mathoverflow/347178 asked by user Biagio Ricceri

theorem mathoverflow_347178 : (∀ n ≥ 2, ∀ (f : EuclideanSpace ℝ (Fin n) → ℝ), ContDiff ℝ 1 f → (BddAbove (Set.range f) ↔ BddAbove (Set.range fun (x : EuclideanSpace ℝ (Fin n)) => f (x + gradient f x))) ∧ ⨆ (x : EuclideanSpace ℝ (Fin n)), ↑(f x) = ⨆ (x : EuclideanSpace ℝ (Fin n)), ↑(f (x + gradient f x))) ↔ sorry

Let $f\colon ℝ^n → ℝ, n ≥ 2$ be a $C^1$ function. Is it true that $$\sup_{x\in {\bf R}^n}f(x)=\sup_{x\in {\bf R}^n}f(x+\nabla f(x))$$?

theorem mathoverflow_347178.variants.bounded_iff : (∀ n ≥ 2, ∀ (f : EuclideanSpace ℝ (Fin n) → ℝ), ContDiff ℝ 1 f → (BddAbove (Set.range f) ↔ BddAbove (Set.range fun (x : EuclideanSpace ℝ (Fin n)) => f (x + gradient f x)))) ↔ sorry

theorem mathoverflow_347178.variants.bounded_only : (∀ n ≥ 2, ∀ (f : EuclideanSpace ℝ (Fin n) → ℝ), ContDiff ℝ 1 f → BddAbove (Set.range f) → BddAbove (Set.range fun (x : EuclideanSpace ℝ (Fin n)) => f (x + gradient f x)) → ⨆ (x : EuclideanSpace ℝ (Fin n)), f x = ⨆ (x : EuclideanSpace ℝ (Fin n)), f (x + gradient f x)) ↔ sorry