Exact source: MathlibAnnex/Analysis/Calculus/FDeriv/SeminormBound.lean
Pinned GitHub source · Raw UTF-8 source
Back to A seminorm increment bound passes to every derivative direction · Back to One boundary extension with all five analytic properties
1import Mathlib.Analysis.Seminorm2import Mathlib.Analysis.Calculus.Rademacher3import Mathlib.Analysis.Calculus.Deriv.Slope4import Mathlib.Analysis.Calculus.Deriv.Comp5import Mathlib.Analysis.Calculus.Deriv.Mul6import Mathlib.Tactic.FieldSimp7import Mathlib.Tactic.Module89/-!10# Directional seminorm bounds for derivatives1112A global increment bound by a seminorm passes to every directional derivative.13The almost everywhere statement uses the reference Lebesgue measure and retains14an arbitrary restricted set, including the model closed unit ball.15-/1617noncomputable section1819open Set MeasureTheory Filter20open scoped Topology2122namespace MathlibAnnex.FDeriv2324/-- A seminorm increment bound passes to the derivative in each direction. -/25theorem norm_apply_le_seminorm_of_lipschitz {n N : ℕ}26 (p : Seminorm ℝ (Fin n → ℝ)) {f : (Fin n → ℝ) → (Fin N → ℝ)}27 (hf : ∀ x y, ‖f x - f y‖ ≤ p (x - y)) {x : Fin n → ℝ}28 (hx : DifferentiableAt ℝ f x) : ∀ v, ‖(fderiv ℝ f x) v‖ ≤ p v := by29 have derivative_bound {φ : ℝ → (Fin N → ℝ)} {d : Fin N → ℝ} {C : ℝ}30 (hφ : HasDerivAt φ d 0)31 (hbound : ∀ t : ℝ, ‖φ t - φ 0‖ ≤ |t| * C) : ‖d‖ ≤ C := by32 have hquot : Tendsto (fun t : ℝ => t⁻¹ • (φ t - φ 0)) (𝓝[≠] 0) (𝓝 d) := by33 simpa using hφ.tendsto_slope_zero34 have hevent : ∀ᶠ t : ℝ in 𝓝[≠] 0, ‖t⁻¹ • (φ t - φ 0)‖ ≤ C := by35 filter_upwards [self_mem_nhdsWithin] with t ht36 have ht0 : t ≠ 0 := ht37 calc38 ‖t⁻¹ • (φ t - φ 0)‖ = |t|⁻¹ * ‖φ t - φ 0‖ := by39 simp [norm_smul, Real.norm_eq_abs]40 _ ≤ |t|⁻¹ * (|t| * C) :=41 mul_le_mul_of_nonneg_left (hbound t) (inv_nonneg.mpr (abs_nonneg t))42 _ = C := by field_simp [abs_ne_zero.mpr ht0]43 exact le_of_tendsto ((continuous_norm.tendsto d).comp hquot) hevent44 intro v45 let φ : ℝ → (Fin N → ℝ) := fun t => f (x + t • v)46 have hφ : HasDerivAt φ ((fderiv ℝ f x) v) 0 := by47 have hline : HasDerivAt (fun t : ℝ => x + t • v) v 0 := by48 simpa using (((hasDerivAt_id (0 : ℝ)).smul_const v).const_add x)49 simpa [φ, Function.comp_def] using50 hx.hasFDerivAt.comp_hasDerivAt_of_eq (0 : ℝ) hline (by simp)51 have hbound : ∀ t : ℝ, ‖φ t - φ 0‖ ≤ |t| * p v := by52 intro t53 calc54 ‖φ t - φ 0‖ ≤ p ((x + t • v) - (x + 0 • v)) := hf _ _55 _ = p (t • v) := by56 exact congrArg (fun w : Fin n → ℝ => p w) (by module)57 _ = |t| * p v := by simpa [Real.norm_eq_abs] using map_smul_eq_mul p t v58 exact derivative_bound hφ hbound5960/-- The directional bound holds almost everywhere on every restricted set. -/61theorem ae_norm_apply_le_seminorm_of_lipschitz {n N : ℕ}62 (p : Seminorm ℝ (Fin n → ℝ)) {f : (Fin n → ℝ) → (Fin N → ℝ)}63 (U : NNReal) (hu : ∀ x, p x ≤ U * ‖x‖)64 (hf : ∀ x y, ‖f x - f y‖ ≤ p (x - y)) (s : Set (Fin n → ℝ)) :65 ∀ᵐ x ∂volume.restrict s, ∀ v, ‖(fderiv ℝ f x) v‖ ≤ p v := by66 have hl : LipschitzWith U f := LipschitzWith.of_dist_le_mul fun x y => by67 simpa [dist_eq_norm] using (hf x y).trans (hu (x - y))68 have hd : ∀ᵐ x ∂volume, DifferentiableAt ℝ f x := hl.ae_differentiableAt69 have hdr : ∀ᵐ x ∂volume.restrict s, DifferentiableAt ℝ f x := ae_restrict_of_ae hd70 filter_upwards [hdr] with x hx71 exact norm_apply_le_seminorm_of_lipschitz p hf hx7273end MathlibAnnex.FDeriv