Continuity and differentiability at the origin in the plane
TheoremThe partial derivatives of \(x^3/(x^2+y^2)\) are bounded#●ready to prove
Let \(f : \mathbb{R}^2 \to \mathbb{R}\) satisfy \(f(0,0)=0\) and \(f(x,y)=x^3/(x^2+y^2)\) for \((x,y)\ne(0,0)\). Then the partial derivatives \(D_1 f\) and \(D_2 f\) are bounded on \(\mathbb{R}^2\): there is a real \(M\) with \(|D_1 f(x,y)| \le M\) for all \(x,y\in\mathbb{R}\), and a real \(M'\) with \(|D_2 f(x,y)| \le M'\) for all \(x,y\in\mathbb{R}\).
public theorem_wanted bounded_partialDerivs_cube_div_sq_add_sq (f : ℝ × ℝ → ℝ) (h0 : f (0, 0) = 0)
(hxy : ∀ p : ℝ × ℝ, p ≠ (0, 0) → f p = (p.1 ^ 3) / (p.1 ^ 2 + p.2 ^ 2)) :
(∃ M : ℝ, ∀ x y : ℝ, ‖deriv (fun t => f (t, y)) x‖ ≤ M) ∧
(∃ M : ℝ, ∀ x y : ℝ, ‖deriv (fun t => f (x, t)) y‖ ≤ M)Sources
- MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of several variables), problem
ma_proofbench_l1_56.
TheoremThe signed radial function is not differentiable at the origin#●ready to prove
Let \(f : \mathbb{R}^2 \to \mathbb{R}\) be the function
Then \(f\) is not differentiable at \((0, 0)\).
public theorem_wanted not_differentiableAt_signed_norm_zero
{f : ℝ × ℝ → ℝ} (hpos : ∀ x y : ℝ, y > 0 → f (x, y) = Real.sqrt (x ^ 2 + y ^ 2))
(hzero : ∀ x : ℝ, f (x, 0) = x)
(hneg : ∀ x y : ℝ, y < 0 → f (x, y) = -Real.sqrt (x ^ 2 + y ^ 2)) :
¬ DifferentiableAt ℝ f (0, 0)Sources
- MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of several variables), problem
ma_proofbench_l1_06.
TheoremThe function \(xy/(x^2+y^2)\) is discontinuous only at the origin#●ready to prove
Let \(f : \mathbb{R}^2 \to \mathbb{R}\) be given by \(f(x,y) = \frac{xy}{x^2+y^2}\) for \((x,y) \neq (0,0)\) and \(f(0,0) = 0\). Then \(f\) is continuous on \(\mathbb{R}^2 \setminus \{(0,0)\}\) and is not continuous at \((0,0)\).
public theorem_wanted continuousOn_compl_and_not_continuousAt_mul_div_sq_add_sq
(f : (ℝ × ℝ) → ℝ)
(hf : (∀ p : (ℝ × ℝ), p ≠ (0, 0) → f p = (p.1 * p.2) / (p.1 ^ (2 : ℕ) + p.2 ^ (2 : ℕ))) ∧
(f (0, 0) = 0)) :
ContinuousOn f ({(0, 0)}ᶜ) ∧ ¬ ContinuousAt f (0, 0)Sources
- MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of several variables), problem
ma_proofbench_l1_93.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.