Mathoverflow 347178

Reference: mathoverflow/347178 asked by user Biagio Ricceri

theorem Mathoverflow347178.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 : \mathbb R^n \to \mathbb R, n \geq 2$ be a $C^1$ function. Is it true that $$\sup_{x \in \mathbb R^n}f(x) = \sup_{x\in \mathbb R^n} f(x+\nabla f(x))$$?

theorem Mathoverflow347178.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

Let $f : \mathbb R^n \to \mathbb R, n \geq 2$ be a $C^1$ function. Is the boundedness of $\sup_{x \in \mathbb R^n}f(x)$ and $\sup_{x\in \mathbb R^n} f(x+\nabla f(x))$ equivalent?

theorem Mathoverflow347178.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

Let $f : \mathbb R^n \to \mathbb R, n \geq 2$ be a $C^1$ function. Does the equality $$\sup_{x \in \mathbb R^n}f(x) = \sup_{x\in \mathbb R^n} f(x+\nabla f(x))$$ hold when both suprema are finite?