Periodic Profile

Gevrey Inverse

theorem EulerGevreyInverse.reciprocal_derivative_recurrence (f : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hnz : ∀ (x : ℝ), f x ≠ 0) (n : ℕ) (x : ℝ) : iteratedDeriv (n + 1) (fun (y : ℝ) => (f y)⁻¹) x = -(f x)⁻¹ * ∑ k ∈ Finset.range (n + 1), ↑((n + 1).choose (k + 1)) * iteratedDeriv (k + 1) f x * iteratedDeriv (n + 1 - (k + 1)) (fun (y : ℝ) => (f y)⁻¹) x

theorem EulerGevreyInverse.reciprocal_gevrey_shift (f : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hnz : ∀ (x : ℝ), f x ≠ 0) (A Rc R : ℝ) (hA : 1 ≤ A) (hRc : 0 ≤ Rc) (hR : 2 * A * (Rc + 1) ≤ R) (hb : ∀ (x : ℝ), |(f x)⁻¹| ≤ A) (hc : ∀ (n : ℕ) (x : ℝ), |iteratedDeriv (n + 1) f x| ≤ EulerGevrey.majorant Rc 0 (n + 1)) (n : ℕ) (x : ℝ) : |iteratedDeriv n (fun (y : ℝ) => (f y)⁻¹) x| ≤ EulerGevrey.majorant R 1 n

theorem EulerGevreyInverse.shift_one_bound (R : ℝ) (hR : 0 ≤ R) (n : ℕ) : EulerGevrey.majorant R 1 n ≤ R * EulerGevrey.majorant (4 * R) 0 n

theorem EulerGevreyInverse.reciprocal_gevrey (f : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hnz : ∀ (x : ℝ), f x ≠ 0) (A Rc R : ℝ) (hA : 1 ≤ A) (hRc : 0 ≤ Rc) (hR : 2 * A * (Rc + 1) ≤ R) (hb : ∀ (x : ℝ), |(f x)⁻¹| ≤ A) (hc : ∀ (n : ℕ) (x : ℝ), |iteratedDeriv (n + 1) f x| ≤ EulerGevrey.majorant Rc 0 (n + 1)) (n : ℕ) (x : ℝ) : |iteratedDeriv n (fun (y : ℝ) => (f y)⁻¹) x| ≤ R * EulerGevrey.majorant (4 * R) 0 n

noncomputable def EulerPeriodicProfile.profile (δ t : ℝ) : ℝ

Explicit smooth periodic profile with a narrow positive derivative peak.

Equations

• EulerPeriodicProfile.profile δ t = Real.arctan (Real.sin t / (1 + δ - Real.cos t))

noncomputable def EulerPeriodicProfile.denominator (δ t : ℝ) : ℝ

Denominator of the derivative of the periodic profile.

Equations

• EulerPeriodicProfile.denominator δ t = (1 + δ) ^ 2 - 2 * (1 + δ) * Real.cos t + 1

theorem EulerPeriodicProfile.first_denominator_pos (δ : ℝ) (hδ : 0 < δ) (t : ℝ) : 0 < 1 + δ - Real.cos t

theorem EulerPeriodicProfile.denominator_lower (δ : ℝ) (hδ : 0 ≤ δ) (t : ℝ) : δ ^ 2 ≤ denominator δ t

theorem EulerPeriodicProfile.denominator_pos (δ : ℝ) (hδ : 0 < δ) (t : ℝ) : 0 < denominator δ t

theorem EulerPeriodicProfile.profile_contDiff (δ : ℝ) (hδ : 0 < δ) : ContDiff ℝ (↑⊤) (profile δ)

theorem EulerPeriodicProfile.profile_odd (δ t : ℝ) : profile δ (-t) = -profile δ t

theorem EulerPeriodicProfile.profile_periodic (δ : ℝ) : Function.Periodic (profile δ) (2 * Real.pi)

theorem EulerPeriodicProfile.profile_hasDerivAt (δ : ℝ) (hδ : 0 < δ) (t : ℝ) : HasDerivAt (profile δ) (((1 + δ) * Real.cos t - 1) / denominator δ t) t

theorem EulerPeriodicProfile.profile_deriv (δ : ℝ) (hδ : 0 < δ) (t : ℝ) : deriv (profile δ) t = ((1 + δ) * Real.cos t - 1) / denominator δ t

theorem EulerPeriodicProfile.profile_deriv_zero (δ : ℝ) (hδ : 0 < δ) : deriv (profile δ) 0 = δ⁻¹

theorem EulerPeriodicProfile.profile_deriv_lower (δ : ℝ) (hδ : 0 < δ) (t : ℝ) : -1 ≤ deriv (profile δ) t

theorem EulerPeriodicProfile.profile_deriv_upper (δ : ℝ) (hδ : 0 < δ) (t : ℝ) : deriv (profile δ) t ≤ δ⁻¹

theorem EulerPeriodicProfile.profile_mean_zero (δ : ℝ) : ∫ (t : ℝ) in -Real.pi..Real.pi, profile δ t = 0

theorem EulerPeriodicProfile.denominator_contDiff (δ : ℝ) : ContDiff ℝ (↑⊤) (denominator δ)

theorem EulerPeriodicProfile.denominator_derivative_bound (δ : ℝ) (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) (n : ℕ) (t : ℝ) : |iteratedDeriv (n + 1) (denominator δ) t| ≤ EulerGevrey.majorant 4 0 (n + 1)

theorem EulerPeriodicProfile.denominator_inverse_bound (δ : ℝ) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (n : ℕ) (t : ℝ) : |iteratedDeriv n (fun (t : ℝ) => (denominator δ t)⁻¹) t| ≤ 10 * (δ ^ 2)⁻¹ * EulerGevrey.majorant (40 * (δ ^ 2)⁻¹) 0 n

noncomputable def EulerPeriodicProfile.numerator (δ t : ℝ) : ℝ

The numerator of the derivative of the explicit periodic profile.

Equations

• EulerPeriodicProfile.numerator δ t = (1 + δ) * Real.cos t - 1

theorem EulerPeriodicProfile.numerator_contDiff (δ : ℝ) : ContDiff ℝ (↑⊤) (numerator δ)

theorem EulerPeriodicProfile.numerator_derivative_bound (δ : ℝ) (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) (n : ℕ) (t : ℝ) : |iteratedDeriv n (numerator δ) t| ≤ 3

theorem EulerPeriodicProfile.profile_gevrey (δ : ℝ) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (n : ℕ) (t : ℝ) : |iteratedDeriv n (profile δ) t| ≤ 100 * (δ ^ 2)⁻¹ * EulerGevrey.majorant (40 * (δ ^ 2)⁻¹) 0 n