def sequentialContinuousAt (U : Set (ℝ × ℝ)) (F : ↑U → ℝ) (p : ↑U) : Prop

Definition 6.3.1: For a set U ⊆ ℝ², a function F : U → ℝ is continuous at (x, y) ∈ U if for every sequence (xₙ, yₙ) of points of U with xₙ → x and yₙ → y, we have F (xₙ, yₙ) → F (x, y). It is continuous if it is continuous at every point of U.

Equations

• One or more equations did not get rendered due to their size.

def sequentialContinuous (U : Set (ℝ × ℝ)) (F : ↑U → ℝ) : Prop

Sequential continuity on U means sequential continuity at every point of U.

Equations

• sequentialContinuous U F = ∀ (p : ↑U), sequentialContinuousAt U F p

theorem tendsto_subtype_coord_iff {U : Set (ℝ × ℝ)} {p : ↑U} {s : ℕ → ↑U} : Filter.Tendsto s Filter.atTop (nhds p) ↔ Filter.Tendsto (fun (n : ℕ) => (↑(s n)).1) Filter.atTop (nhds (↑p).1) ∧ Filter.Tendsto (fun (n : ℕ) => (↑(s n)).2) Filter.atTop (nhds (↑p).2)

theorem sequentialContinuousAt_iff {U : Set (ℝ × ℝ)} {F : ↑U → ℝ} {p : ↑U} : sequentialContinuousAt U F p ↔ ContinuousAt F p

On ℝ × ℝ, sequential continuity at a point agrees with the usual notion of continuity at that point.

theorem sequentialContinuous_iff {U : Set (ℝ × ℝ)} {F : ↑U → ℝ} : sequentialContinuous U F ↔ Continuous F

Sequential continuity on U is equivalent to the usual notion of continuity.

theorem picard_existence_uniqueness {a b c d x₀ : ℝ} (hx₀ : x₀ ∈ Set.Ioo a b) {y₀ : ℝ} (hy₀ : y₀ ∈ Set.Ioo c d) (F : ℝ → ℝ → ℝ) (hcont : ContinuousOn (fun (p : ℝ × ℝ) => F p.1 p.2) (Set.Icc a b ×ˢ Set.Icc c d)) (hLip : ∃ (L : ℝ), 0 ≤ L ∧ ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc c d, ∀ z ∈ Set.Icc c d, |F x y - F x z| ≤ L * |y - z|) : ∃ (h : ℝ), 0 < h ∧ Set.Icc (x₀ - h) (x₀ + h) ⊆ Set.Icc a b ∧ ∃ (f : ℝ → ℝ), ContinuousOn f (Set.Icc (x₀ - h) (x₀ + h)) ∧ (∀ x ∈ Set.Icc (x₀ - h) (x₀ + h), f x ∈ Set.Icc c d) ∧ (∀ x ∈ Set.Ioo (x₀ - h) (x₀ + h), HasDerivAt f (F x (f x)) x) ∧ f x₀ = y₀ ∧ ∀ (g : ℝ → ℝ), ContinuousOn g (Set.Icc (x₀ - h) (x₀ + h)) → (∀ x ∈ Set.Icc (x₀ - h) (x₀ + h), g x ∈ Set.Icc c d) → (∀ x ∈ Set.Ioo (x₀ - h) (x₀ + h), HasDerivAt g (F x (g x)) x) → g x₀ = y₀ → Set.EqOn g f (Set.Icc (x₀ - h) (x₀ + h))

Theorem 6.3.2 (Picard's theorem on existence and uniqueness). Let I = [a,b] and J = [c,d] be closed bounded intervals with interiors (a,b) and (c,d), and take (x₀, y₀) ∈ (a,b) × (c,d). If F : ℝ → ℝ → ℝ is continuous on I × J and Lipschitz in the second variable with constant L ≥ 0, meaning |F x y - F x z| ≤ L * |y - z| for all x ∈ I and y z ∈ J, then there is h > 0 with [x₀ - h, x₀ + h] ⊆ I and a unique differentiable function f : ℝ → ℝ with values in J satisfying f x₀ = y₀ and f' x = F x (f x) on [x₀ - h, x₀ + h].

theorem picard_exponential_example : ∃ (h : ℝ), 0 < h ∧ h < 1 / 2 ∧ ∃ (f : ℝ → ℝ), (∀ x ∈ Set.Icc (-h) h, HasDerivAt f (f x) x) ∧ f 0 = 1 ∧ ∀ (g : ℝ → ℝ), (∀ x ∈ Set.Icc (-h) h, HasDerivAt g (g x) x) ∧ g 0 = 1 → Set.EqOn g f (Set.Icc (-h) h)

Example 6.3.3: Applying Picard's theorem to the initial value problem f' = f with f 0 = 1 (that is, F x y = y) produces some h > 0 with h < 1/2 and a function f : ℝ → ℝ defined on [-h, h] such that f' x = f x on that interval and f 0 = 1, and any other solution with the same initial value agrees with f on [-h, h]. The function extends globally as exp, so the exponential is the unique global solution with that initial value.

theorem exp_unique_solution : ∃! f : ℝ → ℝ, (∀ (x : ℝ), HasDerivAt f (f x) x) ∧ f 0 = 1

The exponential is the unique globally defined solution of the ODE f' = f satisfying f 0 = 1.

theorem one_sub_ne_zero_of_lt {x : ℝ} (hx : x < 1) : 1 - x ≠ 0

theorem hasDerivAt_inv_one_sub {x : ℝ} (hx : x < 1) : HasDerivAt (fun (x : ℝ) => (1 - x)⁻¹) ((1 - x) ^ 2)⁻¹ x

theorem quadratic_ode_example : ∃ (f : ℝ → ℝ), (∀ x < 1, HasDerivAt f (f x ^ 2) x) ∧ f 0 = 1 ∧ ∀ x < 1, f x = (1 - x)⁻¹

Example 6.3.4: For the ODE f' = f ^ 2 with initial condition f 0 = 1, the solution is f x = (1 - x)⁻¹, defined on the interval (-∞, 1). The nonlinearity y ↦ y^2 is not globally Lipschitz, so the guaranteed existence interval from Picard's theorem shrinks as the initial value approaches x = 1.

theorem sqrt_abs_ode_nonunique : ∃ (f : ℝ → ℝ) (g : ℝ → ℝ), f ≠ g ∧ f 0 = 0 ∧ g 0 = 0 ∧ (∀ (x : ℝ), HasDerivAt f (2 * √|f x|) x) ∧ ∀ (x : ℝ), HasDerivAt g (2 * √|g x|) x

Example 6.3.5: For the initial value problem f' x = 2 * √|f x| with f 0 = 0, the right-hand side F x y = 2 * √|y| is continuous but not Lipschitz in y, so uniqueness can fail. The piecewise function f x = x^2 for x ≥ 0 and f x = -x^2 for x < 0 is a solution, while the zero function is another, so a solution exists but is not unique.

noncomputable def dirichletPhi : ℝ → ℝ

Example 6.3.6: Let φ x = 0 when x is rational and φ x = 1 otherwise. The ODE y' = φ has no solution for any initial condition, since the right-hand side is discontinuous and derivatives have the Darboux property, so no differentiable function can have φ as its derivative.

Equations

• dirichletPhi x = if x ∈ Set.range fun (r : ℚ) => ↑r then 0 else 1

theorem dirichletPhi_value_rational {x : ℝ} (hx : x ∈ Set.range fun (r : ℚ) => ↑r) : dirichletPhi x = 0

theorem dirichletPhi_value_irrational {x : ℝ} (hx : x ∉ Set.range fun (r : ℚ) => ↑r) : dirichletPhi x = 1

theorem deriv_eq_dirichletPhi_of_hasDerivAt {f : ℝ → ℝ} {x : ℝ} (h : HasDerivAt f (dirichletPhi x) x) : deriv f x = dirichletPhi x

theorem exists_irrational_in_Ioo_0_1 : ∃ (b : ℝ), 0 < b ∧ b < 1 ∧ Irrational b

theorem no_solution_dirichlet_ode : ¬∃ (f : ℝ → ℝ), Differentiable ℝ f ∧ ∀ (x : ℝ), HasDerivAt f (dirichletPhi x) x

No differentiable function can solve the discontinuous ODE y' = φ where φ is the Dirichlet function. In particular, there is no solution satisfying any prescribed initial value.