1. Physlib
  2. Mathematics
  3. VariationalCalculus
  4. IsLocalizedfunctionTransform
Imports
/- Copyright (c) 2025 Tomas Skrivan. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Tomas Skrivan, Joseph Tooby-Smith -/ module public import Physlib.SpaceAndTime.Space.Derivatives.Div public import Physlib.Mathematics.Calculus.AdjFDeriv

Localized function transforms

In this module we define a locality property for function transforms, F : (X → U) → (Y → V). The locality property IsLocalizedFunctionTransform, says that for every compact set K in Y there exists a compact set L of X, such that if φ and φ' are equal on L, then F φ and F φ' are equal on K.

@[expose] public section

Function transformation F is localizable if the values of the transformed function F φ on some compact set K can depend only on the values of φ on some another compact set L.

def IsLocalizedFunctionTransform (F : (X → U) → (Y → V)) : Prop := ∀ (K : Set Y) (_ : IsCompact K), ∃ L : Set X, IsCompact L ∧ ∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' x
lemma comp {F : (Y → V) → (Z → W)} {G : (X → U) → (Y → V)} (hF : IsLocalizedFunctionTransform F) (hG : IsLocalizedFunctionTransform G) : IsLocalizedFunctionTransform (F ∘ G) := X:Type u_5inst✝²:NormedAddCommGroup XY:Type u_1inst✝¹:NormedAddCommGroup YZ:Type u_2inst✝:NormedAddCommGroup ZU:Sort u_6V:Sort u_3W:Sort u_4F:(Y → V) → Z → WG:(X → U) → Y → VhF:IsLocalizedFunctionTransform FhG:IsLocalizedFunctionTransform G⊢ IsLocalizedFunctionTransform (F ∘ G) X:Type u_5inst✝²:NormedAddCommGroup XY:Type u_1inst✝¹:NormedAddCommGroup YZ:Type u_2inst✝:NormedAddCommGroup ZU:Sort u_6V:Sort u_3W:Sort u_4F:(Y → V) → Z → WG:(X → U) → Y → VhF:IsLocalizedFunctionTransform FhG:IsLocalizedFunctionTransform GK:Set ZcK:IsCompact K⊢ ∃ L, IsCompact L ∧ ∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, (F ∘ G) φ x = (F ∘ G) φ' x X:Type u_5inst✝²:NormedAddCommGroup XY:Type u_1inst✝¹:NormedAddCommGroup YZ:Type u_2inst✝:NormedAddCommGroup ZU:Sort u_6V:Sort u_3W:Sort u_4F:(Y → V) → Z → WG:(X → U) → Y → VhF:IsLocalizedFunctionTransform FhG:IsLocalizedFunctionTransform GK:Set ZcK:IsCompact KK':Set YcK':IsCompact K'h':∀ (φ φ' : Y → V), (∀ x ∈ K', φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' x⊢ ∃ L, IsCompact L ∧ ∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, (F ∘ G) φ x = (F ∘ G) φ' x X:Type u_5inst✝²:NormedAddCommGroup XY:Type u_1inst✝¹:NormedAddCommGroup YZ:Type u_2inst✝:NormedAddCommGroup ZU:Sort u_6V:Sort u_3W:Sort u_4F:(Y → V) → Z → WG:(X → U) → Y → VhF:IsLocalizedFunctionTransform FhG:IsLocalizedFunctionTransform GK:Set ZcK:IsCompact KK':Set YcK':IsCompact K'h':∀ (φ φ' : Y → V), (∀ x ∈ K', φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xK'':Set XcK'':IsCompact K''h'':∀ (φ φ' : X → U), (∀ x ∈ K'', φ x = φ' x) → ∀ x ∈ K', G φ x = G φ' x⊢ ∃ L, IsCompact L ∧ ∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, (F ∘ G) φ x = (F ∘ G) φ' x X:Type u_5inst✝²:NormedAddCommGroup XY:Type u_1inst✝¹:NormedAddCommGroup YZ:Type u_2inst✝:NormedAddCommGroup ZU:Sort u_6V:Sort u_3W:Sort u_4F:(Y → V) → Z → WG:(X → U) → Y → VhF:IsLocalizedFunctionTransform FhG:IsLocalizedFunctionTransform GK:Set ZcK:IsCompact KK':Set YcK':IsCompact K'h':∀ (φ φ' : Y → V), (∀ x ∈ K', φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xK'':Set XcK'':IsCompact K''h'':∀ (φ φ' : X → U), (∀ x ∈ K'', φ x = φ' x) → ∀ x ∈ K', G φ x = G φ' x⊢ IsCompact K'' ∧ ∀ (φ φ' : X → U), (∀ x ∈ K'', φ x = φ' x) → ∀ x ∈ K, (F ∘ G) φ x = (F ∘ G) φ' x X:Type u_5inst✝²:NormedAddCommGroup XY:Type u_1inst✝¹:NormedAddCommGroup YZ:Type u_2inst✝:NormedAddCommGroup ZU:Sort u_6V:Sort u_3W:Sort u_4F:(Y → V) → Z → WG:(X → U) → Y → VhF:IsLocalizedFunctionTransform FhG:IsLocalizedFunctionTransform GK:Set ZcK:IsCompact KK':Set YcK':IsCompact K'h':∀ (φ φ' : Y → V), (∀ x ∈ K', φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xK'':Set XcK'':IsCompact K''h'':∀ (φ φ' : X → U), (∀ x ∈ K'', φ x = φ' x) → ∀ x ∈ K', G φ x = G φ' x⊢ IsCompact K''X:Type u_5inst✝²:NormedAddCommGroup XY:Type u_1inst✝¹:NormedAddCommGroup YZ:Type u_2inst✝:NormedAddCommGroup ZU:Sort u_6V:Sort u_3W:Sort u_4F:(Y → V) → Z → WG:(X → U) → Y → VhF:IsLocalizedFunctionTransform FhG:IsLocalizedFunctionTransform GK:Set ZcK:IsCompact KK':Set YcK':IsCompact K'h':∀ (φ φ' : Y → V), (∀ x ∈ K', φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xK'':Set XcK'':IsCompact K''h'':∀ (φ φ' : X → U), (∀ x ∈ K'', φ x = φ' x) → ∀ x ∈ K', G φ x = G φ' x⊢ ∀ (φ φ' : X → U), (∀ x ∈ K'', φ x = φ' x) → ∀ x ∈ K, (F ∘ G) φ x = (F ∘ G) φ' x X:Type u_5inst✝²:NormedAddCommGroup XY:Type u_1inst✝¹:NormedAddCommGroup YZ:Type u_2inst✝:NormedAddCommGroup ZU:Sort u_6V:Sort u_3W:Sort u_4F:(Y → V) → Z → WG:(X → U) → Y → VhF:IsLocalizedFunctionTransform FhG:IsLocalizedFunctionTransform GK:Set ZcK:IsCompact KK':Set YcK':IsCompact K'h':∀ (φ φ' : Y → V), (∀ x ∈ K', φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xK'':Set XcK'':IsCompact K''h'':∀ (φ φ' : X → U), (∀ x ∈ K'', φ x = φ' x) → ∀ x ∈ K', G φ x = G φ' x⊢ IsCompact K'' All goals completed! 🐙 X:Type u_5inst✝²:NormedAddCommGroup XY:Type u_1inst✝¹:NormedAddCommGroup YZ:Type u_2inst✝:NormedAddCommGroup ZU:Sort u_6V:Sort u_3W:Sort u_4F:(Y → V) → Z → WG:(X → U) → Y → VhF:IsLocalizedFunctionTransform FhG:IsLocalizedFunctionTransform GK:Set ZcK:IsCompact KK':Set YcK':IsCompact K'h':∀ (φ φ' : Y → V), (∀ x ∈ K', φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xK'':Set XcK'':IsCompact K''h'':∀ (φ φ' : X → U), (∀ x ∈ K'', φ x = φ' x) → ∀ x ∈ K', G φ x = G φ' x⊢ ∀ (φ φ' : X → U), (∀ x ∈ K'', φ x = φ' x) → ∀ x ∈ K, (F ∘ G) φ x = (F ∘ G) φ' x X:Type u_5inst✝²:NormedAddCommGroup XY:Type u_1inst✝¹:NormedAddCommGroup YZ:Type u_2inst✝:NormedAddCommGroup ZU:Sort u_6V:Sort u_3W:Sort u_4F:(Y → V) → Z → WG:(X → U) → Y → VhF:IsLocalizedFunctionTransform FhG:IsLocalizedFunctionTransform GK:Set ZcK:IsCompact KK':Set YcK':IsCompact K'h':∀ (φ φ' : Y → V), (∀ x ∈ K', φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xK'':Set XcK'':IsCompact K''h'':∀ (φ φ' : X → U), (∀ x ∈ K'', φ x = φ' x) → ∀ x ∈ K', G φ x = G φ' xφ:X → Uφ':X → Uhφ:∀ x ∈ K'', φ x = φ' x⊢ ∀ x ∈ K, (F ∘ G) φ x = (F ∘ G) φ' x All goals completed! 🐙lemma fun_comp {F : (Y → V) → (Z → W)} {G : (X → U) → (Y → V)} (hF : IsLocalizedFunctionTransform F) (hG : IsLocalizedFunctionTransform G) : IsLocalizedFunctionTransform (fun x => F (G x)) := X:Type u_5inst✝²:NormedAddCommGroup XY:Type u_1inst✝¹:NormedAddCommGroup YZ:Type u_2inst✝:NormedAddCommGroup ZU:Sort u_6V:Sort u_3W:Sort u_4F:(Y → V) → Z → WG:(X → U) → Y → VhF:IsLocalizedFunctionTransform FhG:IsLocalizedFunctionTransform G⊢ IsLocalizedFunctionTransform fun x => F (G x) All goals completed! 🐙All goals completed! 🐙lemma neg {V} [NormedAddCommGroup V] {F : (X → U) → (Y → V)} (hF : IsLocalizedFunctionTransform F) : IsLocalizedFunctionTransform (fun φ => - F φ) := X:Type u_2inst✝²:NormedAddCommGroup XY:Type u_3inst✝¹:NormedAddCommGroup YU:Sort u_4V:Type u_1inst✝:NormedAddCommGroup VF:(X → U) → Y → VhF:IsLocalizedFunctionTransform F⊢ IsLocalizedFunctionTransform fun φ => -F φ X:Type u_2inst✝²:NormedAddCommGroup XY:Type u_3inst✝¹:NormedAddCommGroup YU:Sort u_4V:Type u_1inst✝:NormedAddCommGroup VF:(X → U) → Y → VhF:IsLocalizedFunctionTransform FK:Set YcK:IsCompact K⊢ ∃ L, IsCompact L ∧ ∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, (fun φ => -F φ) φ x = (fun φ => -F φ) φ' x X:Type u_2inst✝²:NormedAddCommGroup XY:Type u_3inst✝¹:NormedAddCommGroup YU:Sort u_4V:Type u_1inst✝:NormedAddCommGroup VF:(X → U) → Y → VhF:IsLocalizedFunctionTransform FK:Set YcK:IsCompact KL:Set XcL:IsCompact Lh:∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' x⊢ ∃ L, IsCompact L ∧ ∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, (fun φ => -F φ) φ x = (fun φ => -F φ) φ' x exact ⟨L,cL,X:Type u_2inst✝²:NormedAddCommGroup XY:Type u_3inst✝¹:NormedAddCommGroup YU:Sort u_4V:Type u_1inst✝:NormedAddCommGroup VF:(X → U) → Y → VhF:IsLocalizedFunctionTransform FK:Set YcK:IsCompact KL:Set XcL:IsCompact Lh:∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' x⊢ ∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, (fun φ => -F φ) φ x = (fun φ => -F φ) φ' x X:Type u_2inst✝²:NormedAddCommGroup XY:Type u_3inst✝¹:NormedAddCommGroup YU:Sort u_4V:Type u_1inst✝:NormedAddCommGroup VF:(X → U) → Y → VhF:IsLocalizedFunctionTransform FK:Set YcK:IsCompact KL:Set XcL:IsCompact Lh:∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xφ✝:X → Uφ'✝:X → Ua✝¹:∀ x ∈ L, φ✝ x = φ'✝ xx✝:Ya✝:x✝ ∈ K⊢ (fun φ => -F φ) φ✝ x✝ = (fun φ => -F φ) φ'✝ x✝; X:Type u_2inst✝²:NormedAddCommGroup XY:Type u_3inst✝¹:NormedAddCommGroup YU:Sort u_4V:Type u_1inst✝:NormedAddCommGroup VF:(X → U) → Y → VhF:IsLocalizedFunctionTransform FK:Set YcK:IsCompact KL:Set XcL:IsCompact Lh:∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xφ✝:X → Uφ'✝:X → Ua✝¹:∀ x ∈ L, φ✝ x = φ'✝ xx✝:Ya✝:x✝ ∈ K⊢ -F φ✝ x✝ = -F φ'✝ x✝; X:Type u_2inst✝²:NormedAddCommGroup XY:Type u_3inst✝¹:NormedAddCommGroup YU:Sort u_4V:Type u_1inst✝:NormedAddCommGroup VF:(X → U) → Y → VhF:IsLocalizedFunctionTransform FK:Set YcK:IsCompact KL:Set XcL:IsCompact Lh:∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xφ✝:X → Uφ'✝:X → Ua✝¹:∀ x ∈ L, φ✝ x = φ'✝ xx✝:Ya✝:x✝ ∈ K⊢ F φ✝ x✝ = F φ'✝ x✝; X:Type u_2inst✝²:NormedAddCommGroup XY:Type u_3inst✝¹:NormedAddCommGroup YU:Sort u_4V:Type u_1inst✝:NormedAddCommGroup VF:(X → U) → Y → VhF:IsLocalizedFunctionTransform FK:Set YcK:IsCompact KL:Set XcL:IsCompact Lh:∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xφ✝:X → Uφ'✝:X → Ua✝¹:∀ x ∈ L, φ✝ x = φ'✝ xx✝:Ya✝:x✝ ∈ K⊢ ∀ x ∈ L, φ✝ x = φ'✝ xX:Type u_2inst✝²:NormedAddCommGroup XY:Type u_3inst✝¹:NormedAddCommGroup YU:Sort u_4V:Type u_1inst✝:NormedAddCommGroup VF:(X → U) → Y → VhF:IsLocalizedFunctionTransform FK:Set YcK:IsCompact KL:Set XcL:IsCompact Lh:∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xφ✝:X → Uφ'✝:X → Ua✝¹:∀ x ∈ L, φ✝ x = φ'✝ xx✝:Ya✝:x✝ ∈ K⊢ x✝ ∈ K X:Type u_2inst✝²:NormedAddCommGroup XY:Type u_3inst✝¹:NormedAddCommGroup YU:Sort u_4V:Type u_1inst✝:NormedAddCommGroup VF:(X → U) → Y → VhF:IsLocalizedFunctionTransform FK:Set YcK:IsCompact KL:Set XcL:IsCompact Lh:∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xφ✝:X → Uφ'✝:X → Ua✝¹:∀ x ∈ L, φ✝ x = φ'✝ xx✝:Ya✝:x✝ ∈ K⊢ ∀ x ∈ L, φ✝ x = φ'✝ xX:Type u_2inst✝²:NormedAddCommGroup XY:Type u_3inst✝¹:NormedAddCommGroup YU:Sort u_4V:Type u_1inst✝:NormedAddCommGroup VF:(X → U) → Y → VhF:IsLocalizedFunctionTransform FK:Set YcK:IsCompact KL:Set XcL:IsCompact Lh:∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xφ✝:X → Uφ'✝:X → Ua✝¹:∀ x ∈ L, φ✝ x = φ'✝ xx✝:Ya✝:x✝ ∈ K⊢ x✝ ∈ K All goals completed! 🐙⟩X:Type u_2inst✝²:NormedAddCommGroup XY:Type u_3inst✝¹:NormedAddCommGroup YU:Sort u_4V:Type u_1inst✝:NormedAddCommGroup VF:(X → U) → Y → VG:(X → U) → Y → VhF:IsLocalizedFunctionTransform FhG:IsLocalizedFunctionTransform GK:Set YcK:IsCompact KL:Set XcL:IsCompact Lh:∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xL':Set XcL':IsCompact L'h':∀ (φ φ' : X → U), (∀ x ∈ L', φ x = φ' x) → ∀ x ∈ K, G φ x = G φ' xφ:X → Uφ':X → Uhφ:∀ x ∈ L ∪ L', φ x = φ' xhL:∀ x ∈ L, φ x = φ' xhL':∀ x ∈ L', φ x = φ' x⊢ ∀ x ∈ K, (fun φ => F φ + G φ) φ x = (fun φ => F φ + G φ) φ' x All goals completed! 🐙All goals completed! 🐙⟩All goals completed! 🐙⟩All goals completed! 🐙⟩d:ℕK:Set (Space d)cK:IsCompact Kφ:Space d → EuclideanSpace ℝ (Fin d)φ':Space d → EuclideanSpace ℝ (Fin d)hφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xh:∀ (i : Fin d), ∀ x ∈ K, (fun x => (φ x).ofLp i) =ᶠ[nhds x] fun x => (φ' x).ofLp i⊢ ∀ x ∈ K, (fun φ x => Space.div φ x) φ x = (fun φ x => Space.div φ x) φ' x d:ℕK:Set (Space d)cK:IsCompact Kφ:Space d → EuclideanSpace ℝ (Fin d)φ':Space d → EuclideanSpace ℝ (Fin d)hφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xh:∀ (i : Fin d), ∀ x ∈ K, (fun x => (φ x).ofLp i) =ᶠ[nhds x] fun x => (φ' x).ofLp ix:Space dhx:x ∈ K⊢ (fun φ x => Space.div φ x) φ x = (fun φ x => Space.div φ x) φ' x; d:ℕK:Set (Space d)cK:IsCompact Kφ:Space d → EuclideanSpace ℝ (Fin d)φ':Space d → EuclideanSpace ℝ (Fin d)hφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xh:∀ (i : Fin d), ∀ x ∈ K, (fun x => (φ x).ofLp i) =ᶠ[nhds x] fun x => (φ' x).ofLp ix:Space dhx:x ∈ K⊢ Space.div φ x = Space.div φ' x; d:ℕK:Set (Space d)cK:IsCompact Kφ:Space d → EuclideanSpace ℝ (Fin d)φ':Space d → EuclideanSpace ℝ (Fin d)hφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xh:∀ (i : Fin d), ∀ x ∈ K, (fun x => (φ x).ofLp i) =ᶠ[nhds x] fun x => (φ' x).ofLp ix:Space dhx:x ∈ K⊢ ∑ x_1, (fderiv ℝ (fun x => (φ x).ofLp x_1) x) (Space.basis x_1) = ∑ x_1, (fderiv ℝ (fun x => (φ' x).ofLp x_1) x) (Space.basis x_1) d:ℕK:Set (Space d)cK:IsCompact Kφ:Space d → EuclideanSpace ℝ (Fin d)φ':Space d → EuclideanSpace ℝ (Fin d)hφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xh:∀ (i : Fin d), ∀ x ∈ K, (fun x => (φ x).ofLp i) =ᶠ[nhds x] fun x => (φ' x).ofLp ix:Space dhx:x ∈ K⊢ (fun x_1 => (fderiv ℝ (fun x => (φ x).ofLp x_1) x) (Space.basis x_1)) = fun x_1 => (fderiv ℝ (fun x => (φ' x).ofLp x_1) x) (Space.basis x_1); d:ℕK:Set (Space d)cK:IsCompact Kφ:Space d → EuclideanSpace ℝ (Fin d)φ':Space d → EuclideanSpace ℝ (Fin d)hφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xh:∀ (i : Fin d), ∀ x ∈ K, (fun x => (φ x).ofLp i) =ᶠ[nhds x] fun x => (φ' x).ofLp ix:Space dhx:x ∈ Ki:Fin d⊢ (fderiv ℝ (fun x => (φ x).ofLp i) x) (Space.basis i) = (fderiv ℝ (fun x => (φ' x).ofLp i) x) (Space.basis i); d:ℕK:Set (Space d)cK:IsCompact Kφ:Space d → EuclideanSpace ℝ (Fin d)φ':Space d → EuclideanSpace ℝ (Fin d)hφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xh:∀ (i : Fin d), ∀ x ∈ K, (fun x => (φ x).ofLp i) =ᶠ[nhds x] fun x => (φ' x).ofLp ix:Space dhx:x ∈ Ki:Fin d⊢ fderiv ℝ (fun x => (φ x).ofLp i) x = fderiv ℝ (fun x => (φ' x).ofLp i) x All goals completed! 🐙d:ℕK:Set (Space d)cK:IsCompact Kφ:Space d → Space dφ':Space d → Space dhφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xh:∀ (i : Fin d), ∀ x ∈ K, (fun x => (φ x).val i) =ᶠ[nhds x] fun x => (φ' x).val i⊢ ∀ x ∈ K, (fun φ x => Space.div (⇑Space.basis.repr ∘ φ) x) φ x = (fun φ x => Space.div (⇑Space.basis.repr ∘ φ) x) φ' x d:ℕK:Set (Space d)cK:IsCompact Kφ:Space d → Space dφ':Space d → Space dhφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xh:∀ (i : Fin d), ∀ x ∈ K, (fun x => (φ x).val i) =ᶠ[nhds x] fun x => (φ' x).val ix:Space dhx:x ∈ K⊢ (fun φ x => Space.div (⇑Space.basis.repr ∘ φ) x) φ x = (fun φ x => Space.div (⇑Space.basis.repr ∘ φ) x) φ' x; d:ℕK:Set (Space d)cK:IsCompact Kφ:Space d → Space dφ':Space d → Space dhφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xh:∀ (i : Fin d), ∀ x ∈ K, (fun x => (φ x).val i) =ᶠ[nhds x] fun x => (φ' x).val ix:Space dhx:x ∈ K⊢ Space.div (⇑Space.basis.repr ∘ φ) x = Space.div (⇑Space.basis.repr ∘ φ') x; d:ℕK:Set (Space d)cK:IsCompact Kφ:Space d → Space dφ':Space d → Space dhφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xh:∀ (i : Fin d), ∀ x ∈ K, (fun x => (φ x).val i) =ᶠ[nhds x] fun x => (φ' x).val ix:Space dhx:x ∈ K⊢ ∑ x_1, (fderiv ℝ (fun x => (φ x).val x_1) x) (Space.basis x_1) = ∑ x_1, (fderiv ℝ (fun x => (φ' x).val x_1) x) (Space.basis x_1) d:ℕK:Set (Space d)cK:IsCompact Kφ:Space d → Space dφ':Space d → Space dhφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xh:∀ (i : Fin d), ∀ x ∈ K, (fun x => (φ x).val i) =ᶠ[nhds x] fun x => (φ' x).val ix:Space dhx:x ∈ K⊢ (fun x_1 => (fderiv ℝ (fun x => (φ x).val x_1) x) (Space.basis x_1)) = fun x_1 => (fderiv ℝ (fun x => (φ' x).val x_1) x) (Space.basis x_1); d:ℕK:Set (Space d)cK:IsCompact Kφ:Space d → Space dφ':Space d → Space dhφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xh:∀ (i : Fin d), ∀ x ∈ K, (fun x => (φ x).val i) =ᶠ[nhds x] fun x => (φ' x).val ix:Space dhx:x ∈ Ki:Fin d⊢ (fderiv ℝ (fun x => (φ x).val i) x) (Space.basis i) = (fderiv ℝ (fun x => (φ' x).val i) x) (Space.basis i); d:ℕK:Set (Space d)cK:IsCompact Kφ:Space d → Space dφ':Space d → Space dhφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xh:∀ (i : Fin d), ∀ x ∈ K, (fun x => (φ x).val i) =ᶠ[nhds x] fun x => (φ' x).val ix:Space dhx:x ∈ Ki:Fin d⊢ fderiv ℝ (fun x => (φ x).val i) x = fderiv ℝ (fun x => (φ' x).val i) x All goals completed! 🐙d:ℕK:Set (Space d)cK:IsCompact Kφ:Space d → ℝφ':Space d → ℝhφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xx:Space dhx:x ∈ Ki:Fin dh:φ =ᶠ[nhds x] φ'⊢ fderiv ℝ φ x = fderiv ℝ φ' x All goals completed! 🐙d:ℕK:Set (Space d)cK:IsCompact Kφ:Space d → ℝφ':Space d → ℝhφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xx:Space dhx:x ∈ Ki:Fin dh:φ =ᶠ[nhds x] φ'⊢ fderiv ℝ φ x = fderiv ℝ φ' x All goals completed! 🐙lemma clm_apply [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup U] [NormedSpace ℝ U] (f : X → (U →L[ℝ] V)) : IsLocalizedFunctionTransform fun φ x => (f x) (φ x) := X:Type u_3inst✝⁴:NormedAddCommGroup XU:Type u_2V:Type u_1inst✝³:NormedAddCommGroup Vinst✝²:NormedSpace ℝ Vinst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → U →L[ℝ] V⊢ IsLocalizedFunctionTransform fun φ x => (f x) (φ x) X:Type u_3inst✝⁴:NormedAddCommGroup XU:Type u_2V:Type u_1inst✝³:NormedAddCommGroup Vinst✝²:NormedSpace ℝ Vinst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → U →L[ℝ] VK:Set XcK:IsCompact K⊢ ∃ L, IsCompact L ∧ ∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, (fun φ x => (f x) (φ x)) φ x = (fun φ x => (f x) (φ x)) φ' x exact ⟨K, cK, X:Type u_3inst✝⁴:NormedAddCommGroup XU:Type u_2V:Type u_1inst✝³:NormedAddCommGroup Vinst✝²:NormedSpace ℝ Vinst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → U →L[ℝ] VK:Set XcK:IsCompact K⊢ ∀ (φ φ' : X → U), (∀ x ∈ K, φ x = φ' x) → ∀ x ∈ K, (fun φ x => (f x) (φ x)) φ x = (fun φ x => (f x) (φ x)) φ' x X:Type u_3inst✝⁴:NormedAddCommGroup XU:Type u_2V:Type u_1inst✝³:NormedAddCommGroup Vinst✝²:NormedSpace ℝ Vinst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ Uf:X → U →L[ℝ] VK:Set XcK:IsCompact Kφ✝:X → Uφ'✝:X → Uhφ:∀ x ∈ K, φ✝ x = φ'✝ xx✝:Xa✝:x✝ ∈ K⊢ (fun φ x => (f x) (φ x)) φ✝ x✝ = (fun φ x => (f x) (φ x)) φ'✝ x✝; All goals completed! 🐙⟩U:Type u_1inst✝¹:NormedAddCommGroup Uinst✝:NormedSpace ℝ UK:Set ℝcK:IsCompact Kφ:ℝ → Uφ':ℝ → Uhφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xx:ℝhx:x ∈ Kh:φ =ᶠ[nhds x] φ'⊢ _root_.deriv φ x = _root_.deriv φ' x All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙⟩All goals completed! 🐙⟩X:Type u_2inst✝:NormedAddCommGroup XU:Sort u_3V:Type u_4W:Type u_1F:(X → U) → X → WG:(X → U) → X → VhF✝:IsLocalizedFunctionTransform FhG✝:IsLocalizedFunctionTransform GK:Set XcK:IsCompact KA:Set XcA:IsCompact AhF:∀ (φ φ' : X → U), (∀ x ∈ A, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xB:Set XcB:IsCompact BhG:∀ (φ φ' : X → U), (∀ x ∈ B, φ x = φ' x) → ∀ x ∈ K, G φ x = G φ' xφ:X → Uφ':X → Uh:∀ x ∈ A ∪ B, φ x = φ' xx:Xhx:x ∈ K⊢ ∀ x ∈ B, φ x = φ' xX:Type u_2inst✝:NormedAddCommGroup XU:Sort u_3V:Type u_4W:Type u_1F:(X → U) → X → WG:(X → U) → X → VhF✝:IsLocalizedFunctionTransform FhG✝:IsLocalizedFunctionTransform GK:Set XcK:IsCompact KA:Set XcA:IsCompact AhF:∀ (φ φ' : X → U), (∀ x ∈ A, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xB:Set XcB:IsCompact BhG:∀ (φ φ' : X → U), (∀ x ∈ B, φ x = φ' x) → ∀ x ∈ K, G φ x = G φ' xφ:X → Uφ':X → Uh:∀ x ∈ A ∪ B, φ x = φ' xx:Xhx:x ∈ K⊢ x ∈ KX:Type u_2inst✝:NormedAddCommGroup XU:Sort u_3V:Type u_4W:Type u_1F:(X → U) → X → WG:(X → U) → X → VhF✝:IsLocalizedFunctionTransform FhG✝:IsLocalizedFunctionTransform GK:Set XcK:IsCompact KA:Set XcA:IsCompact AhF:∀ (φ φ' : X → U), (∀ x ∈ A, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xB:Set XcB:IsCompact BhG:∀ (φ φ' : X → U), (∀ x ∈ B, φ x = φ' x) → ∀ x ∈ K, G φ x = G φ' xφ:X → Uφ':X → Uh:∀ x ∈ A ∪ B, φ x = φ' xx:Xhx:x ∈ K⊢ ∀ x ∈ A, φ x = φ' xX:Type u_2inst✝:NormedAddCommGroup XU:Sort u_3V:Type u_4W:Type u_1F:(X → U) → X → WG:(X → U) → X → VhF✝:IsLocalizedFunctionTransform FhG✝:IsLocalizedFunctionTransform GK:Set XcK:IsCompact KA:Set XcA:IsCompact AhF:∀ (φ φ' : X → U), (∀ x ∈ A, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xB:Set XcB:IsCompact BhG:∀ (φ φ' : X → U), (∀ x ∈ B, φ x = φ' x) → ∀ x ∈ K, G φ x = G φ' xφ:X → Uφ':X → Uh:∀ x ∈ A ∪ B, φ x = φ' xx:Xhx:x ∈ K⊢ x ∈ K X:Type u_2inst✝:NormedAddCommGroup XU:Sort u_3V:Type u_4W:Type u_1F:(X → U) → X → WG:(X → U) → X → VhF✝:IsLocalizedFunctionTransform FhG✝:IsLocalizedFunctionTransform GK:Set XcK:IsCompact KA:Set XcA:IsCompact AhF:∀ (φ φ' : X → U), (∀ x ∈ A, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xB:Set XcB:IsCompact BhG:∀ (φ φ' : X → U), (∀ x ∈ B, φ x = φ' x) → ∀ x ∈ K, G φ x = G φ' xφ:X → Uφ':X → Uh:∀ x ∈ A ∪ B, φ x = φ' xx:Xhx:x ∈ K⊢ ∀ x ∈ B, φ x = φ' xX:Type u_2inst✝:NormedAddCommGroup XU:Sort u_3V:Type u_4W:Type u_1F:(X → U) → X → WG:(X → U) → X → VhF✝:IsLocalizedFunctionTransform FhG✝:IsLocalizedFunctionTransform GK:Set XcK:IsCompact KA:Set XcA:IsCompact AhF:∀ (φ φ' : X → U), (∀ x ∈ A, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xB:Set XcB:IsCompact BhG:∀ (φ φ' : X → U), (∀ x ∈ B, φ x = φ' x) → ∀ x ∈ K, G φ x = G φ' xφ:X → Uφ':X → Uh:∀ x ∈ A ∪ B, φ x = φ' xx:Xhx:x ∈ K⊢ x ∈ KX:Type u_2inst✝:NormedAddCommGroup XU:Sort u_3V:Type u_4W:Type u_1F:(X → U) → X → WG:(X → U) → X → VhF✝:IsLocalizedFunctionTransform FhG✝:IsLocalizedFunctionTransform GK:Set XcK:IsCompact KA:Set XcA:IsCompact AhF:∀ (φ φ' : X → U), (∀ x ∈ A, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xB:Set XcB:IsCompact BhG:∀ (φ φ' : X → U), (∀ x ∈ B, φ x = φ' x) → ∀ x ∈ K, G φ x = G φ' xφ:X → Uφ':X → Uh:∀ x ∈ A ∪ B, φ x = φ' xx:Xhx:x ∈ K⊢ ∀ x ∈ A, φ x = φ' xX:Type u_2inst✝:NormedAddCommGroup XU:Sort u_3V:Type u_4W:Type u_1F:(X → U) → X → WG:(X → U) → X → VhF✝:IsLocalizedFunctionTransform FhG✝:IsLocalizedFunctionTransform GK:Set XcK:IsCompact KA:Set XcA:IsCompact AhF:∀ (φ φ' : X → U), (∀ x ∈ A, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' xB:Set XcB:IsCompact BhG:∀ (φ φ' : X → U), (∀ x ∈ B, φ x = φ' x) → ∀ x ∈ K, G φ x = G φ' xφ:X → Uφ':X → Uh:∀ x ∈ A ∪ B, φ x = φ' xx:Xhx:x ∈ K⊢ x ∈ K All goals completed! 🐙X:Type u_1inst✝⁶:NormedAddCommGroup XY:Type u_2inst✝⁵:NormedAddCommGroup Yinst✝⁴:NormedSpace ℝ Ydy:Yinst✝³:NormedSpace ℝ Xinst✝²:ProperSpace Xinst✝¹:InnerProductSpace' ℝ Xinst✝:InnerProductSpace' ℝ YK:Set XcK:IsCompact Kφ:X → Yφ':X → Yhφ:∀ x ∈ Metric.cthickening 1 K, φ x = φ' xx:Xhx:x ∈ Kh:φ =ᶠ[nhds x] φ'⊢ _root_.fderiv ℝ φ x = _root_.fderiv ℝ φ' x All goals completed! 🐙