OAI/MathematicalPhysics/Elasticity/Parameters.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ElasticityPlanar.PL2 line 12
2. lemma OAI.ElasticityPlanar.lp_dist_add line 14
3. lemma OAI.ElasticityPlanar.lp_dist_smul line 16
4. lemma OAI.ElasticityPlanar.lp_dist_sum line 19
5. theorem OAI.ElasticityPlanar.exists_matrix_multiplier line 24

   Source documentation

   The matrix multiplication here acts on genuine L2 classes and agrees with multiplication on distributions; it is not a formal bounded-operator model.

   theorem exists_matrix_multiplier (a : n → n → ℂ → ℂ)
       (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j))
       (hc : ∀ i j, HasCompactSupport (a i j)) :
       ∃ M : Hilbert n →L[ℂ] Hilbert n, ∀ (f : Hilbert n) (i : n),
         (M f i : 𝓢'(ℂ,ℂ))=∑ j, smulLeftCLM ℂ (a i j) (f j : 𝓢'(ℂ,ℂ)) := by
   …

   Mentions: OAI.ElasticityPlanar.Hilbert

6. theorem OAI.ElasticityPlanar.exists_planar_distribution_inverse line 43
7. theorem OAI.ElasticityPlanar.local_homotopy_inverse line 55

   Source documentation

   Local smooth dependence of an actual distributional planar inverse along the coefficient homotopy s*a. This supplies the parameter ingredient for frame construction without invoking holomorphic bundle triviality.

   theorem local_homotopy_inverse {S Ω : Set ℂ} (hS : IsCompact S) (hΩ : Ω ⊆ S)
       (a : n → n → ℂ → ℂ) (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j))
       (hc : ∀ i j, HasCompactSupport (a i j)) (s₀ : ℝ) :
       ∃ (U : Set ℝ) (T : ℝ → Hilbert n →L[ℂ] Hilbert n),
         IsOpen U ∧ s₀ ∈ U ∧ ContDiffOn ℝ (⊤ : ℕ∞) T U ∧
         ∀ s ∈ U, ∀ f : Hilbert n, ∀ i,
           LocalEqual Ω (ElasticityPlanarDistribution.dbar (T s f i : 𝓢'(ℂ,ℂ))+
             ∑ j, smulLeftCLM ℂ (fun z => (s : ℂ)*a i j z)
               (T s f j : 𝓢'(ℂ,ℂ))) (f i : 𝓢'(ℂ,ℂ)) := by
   …

   Mentions: OAI.ElasticityPlanar.Hilbert, OAI.ElasticityPlanarDistribution.dbar

8. def OAI.ElasticityPlanar.entryInjection line 141
9. lemma OAI.ElasticityPlanar.entryInjection_apply line 145
10. def OAI.ElasticityPlanar.planarOperator line 147
11. lemma OAI.ElasticityPlanar.planarOperator_apply line 151
12. theorem OAI.ElasticityPlanar.global_homotopy_inverse line 160

    Source documentation

    A genuine smooth bounded weak inverse along the entire real homotopy. The patching uses a proved smooth convex selection theorem from Mathlib; it adds no global frame or invertibility assumption to the PDE.

    theorem global_homotopy_inverse {S Ω : Set ℂ} (hS : IsCompact S) (hΩ : Ω ⊆ S)
        (a : n → n → ℂ → ℂ) (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j))
        (hc : ∀ i j, HasCompactSupport (a i j)) :
        ∃ T : ℝ → Hilbert n →L[ℂ] Hilbert n,
          ContDiff ℝ (⊤ : ℕ∞) T ∧ ∀ s, ∀ f : Hilbert n, ∀ i,
          LocalEqual Ω (ElasticityPlanarDistribution.dbar (T s f i : 𝓢'(ℂ,ℂ))+
            ∑ j, smulLeftCLM ℂ (fun z => (s : ℂ)*a i j z) (T s f j : 𝓢'(ℂ,ℂ)))
            (f i : 𝓢'(ℂ,ℂ)) := by
    …

    Mentions: OAI.ElasticityPlanar.Hilbert, OAI.ElasticityPlanarDistribution.dbar

13. lemma OAI.ElasticityRegularity.complex_clm_apply_smooth line 199
14. lemma OAI.ElasticityRegularity.complex_clm_comp_smooth line 204
15. theorem OAI.ElasticityPlanar.exists_smooth_matrix_multiplier line 214
16. theorem OAI.ElasticityPlanar.local_variable_inverse line 239

    Source documentation

    Local inversion for an arbitrary joint smooth compact coefficient family, not merely scalar multiples of one coefficient.

    theorem local_variable_inverse {S Ω K : Set ℂ} (hS : IsCompact S) (hΩ : Ω ⊆ S)
        (hK : IsCompact K) (a : n → n → P × ℂ → ℂ)
        (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j))
        (hs : ∀ i j p z, z∉K → a i j (p,z)=0) (p₀ : P) :
        ∃ (U : Set P) (T : P → Hilbert n →L[ℂ] Hilbert n),
          IsOpen U ∧ p₀∈U ∧ ContDiffOn ℝ (⊤ : ℕ∞) T U ∧
          ∀ p∈U, ∀ (f : Hilbert n) i,
            LocalEqual Ω (planarOperator (fun i j z => a i j (p,z)) i (T p f)) (f i : 𝓢'(ℂ,ℂ)) := by
    …

    Mentions: OAI.ElasticityPlanar.Hilbert, OAI.ElasticityPlanar.planarOperator

17. theorem OAI.ElasticityPlanar.global_variable_inverse line 304

    Source documentation

    A global smooth weak right inverse for actual smooth compactly supported matrix coefficients over any finite-dimensional real parameter space.

    theorem global_variable_inverse {S Ω K : Set ℂ} (hS : IsCompact S) (hΩ : Ω ⊆ S)
        (hK : IsCompact K) (a : n → n → P × ℂ → ℂ)
        (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j))
        (hs : ∀ i j p z, z∉K → a i j (p,z)=0) :
        ∃ T : P → Hilbert n →L[ℂ] Hilbert n,
          ContDiff ℝ (⊤ : ℕ∞) T ∧ ∀ p, ∀ f : Hilbert n, ∀ i,
          LocalEqual Ω (planarOperator (fun i j z => a i j (p,z)) i (T p f)) (f i : 𝓢'(ℂ,ℂ)) := by
    …

    Mentions: OAI.ElasticityPlanar.Hilbert, OAI.ElasticityPlanar.planarOperator

18. theorem OAI.ElasticityRegularity.quantitative_laplacian_gain line 339

    Source documentation

    The actual whole-space Laplacian gain has a uniform norm estimate. Its constant does not depend on any conjugation parameter or on the unknown.

    theorem quantitative_laplacian_gain (s : ℝ) :
        ∃ C : ℝ, 0<C ∧ ∀ f g : Lp ℂ 2 (volume : Measure E),
          Δ (sobolevInjection s f)=sobolevInjection (s-1) g →
          ∃ q : Lp ℂ 2 (volume : Measure E),
            sobolevInjection (s+1) q=sobolevInjection s f ∧
            ‖q‖ ≤ C*(‖f‖+‖g‖) := by
    …

    Mentions: OAI.ElasticityRegularity.sobolevInjection

19. theorem OAI.ElasticityRegularity.bounded_laplacian_graph_gain line 388

    Source documentation

    A bounded realization of the actual Laplacian graph gain, extended by orthogonal projection only off its graph. On the graph it is the unique actual Sobolev representative. This is used for strong parameter regularity.

    theorem bounded_laplacian_graph_gain (s : ℝ) :
        ∃ L : (Lp ℂ 2 (volume : Measure E) × Lp ℂ 2 (volume : Measure E)) →L[ℂ]
            Lp ℂ 2 (volume : Measure E),
          ∀ f g, Δ (sobolevInjection s f)=sobolevInjection (s-1) g →
            sobolevInjection (s+1) (L (f,g))=sobolevInjection s f := by
    …

    Mentions: OAI.ElasticityRegularity.sobolevInjection

20. theorem OAI.ElasticityRegularity.smooth_laplacian_gain line 437
21. def OAI.ElasticityRegularity.SmoothSobolev line 456

    Source documentation

    Smooth dependence in the genuine Hilbert Sobolev topology, with the representative tied to the given distribution family.

    def SmoothSobolev (s : ℝ) (u : P → 𝓢'(E,ℂ)) : Prop :=
    …

22. def OAI.ElasticityRegularity.SmoothLocalSobolev line 460
23. lemma OAI.ElasticityRegularity.SmoothSobolev.add line 466
24. lemma OAI.ElasticityRegularity.SmoothSobolev.sub line 471
25. lemma OAI.ElasticityRegularity.SmoothSobolev.smul line 476
26. lemma OAI.ElasticityRegularity.SmoothSobolev.zero line 480
27. lemma OAI.ElasticityRegularity.SmoothSobolev.sum line 482
28. lemma OAI.ElasticityRegularity.SmoothSobolev.mono line 492
29. lemma OAI.ElasticityRegularity.SmoothSobolev.derivative line 496
30. lemma OAI.ElasticityRegularity.SmoothSobolev.laplacian_gain line 501
31. lemma OAI.ElasticityRegularity.SmoothLocalSobolev.add line 511
32. lemma OAI.ElasticityRegularity.SmoothLocalSobolev.sub line 515
33. lemma OAI.ElasticityRegularity.SmoothLocalSobolev.smul line 519
34. lemma OAI.ElasticityRegularity.SmoothLocalSobolev.sum line 523
35. lemma OAI.ElasticityRegularity.SmoothLocalSobolev.mono line 529
36. lemma OAI.ElasticityRegularity.SmoothLocalSobolev.coeff line 531
37. lemma OAI.ElasticityRegularity.SmoothLocalSobolev.product_derivative line 536
38. lemma OAI.ElasticityRegularity.SmoothLocalSobolev.derivative line 546
39. lemma OAI.ElasticityRegularity.SmoothLocalSobolev.congr line 549
40. lemma OAI.ElasticityRegularity.SmoothLocalSobolev.laplacian_gain line 559

    Source documentation

    Strong smooth parameter regularity is gained for the actual distribution family; the proof uses fixed bounded Laplacian graph operators.

    lemma laplacian_gain (hu : SmoothLocalSobolev Ω s u)
        (hΔ : SmoothLocalSobolev Ω (s-1) (fun p => Δ (u p))) :
        SmoothLocalSobolev Ω (s+1) u := by
    …

    Mentions: OAI.ElasticityRegularity.SmoothLocalSobolev

41. lemma OAI.ElasticityRegularity.smooth_spatial_derivative line 586
42. lemma OAI.ElasticityRegularity.compact_slice line 602
43. lemma OAI.ElasticityRegularity.spatial_derivative_outside line 609
44. lemma OAI.ElasticityRegularity.SmoothSobolev.coordinate_gain line 620
45. lemma OAI.ElasticityRegularity.SmoothSobolev.variable_zero line 630
46. theorem OAI.ElasticityRegularity.SmoothSobolev.variable_nat line 661

    Source documentation

    Joint smooth coefficient multiplication in the strong Hilbert Sobolev parameter topology, for each actual nonnegative integral order.

    theorem SmoothSobolev.variable_nat {S : Set E} (hS : IsCompact S)
        (N : ℕ) (a : P × E → ℂ) (ha : ContDiff ℝ (⊤ : ℕ∞) a)
        (hs : ∀ p x, x∉S → a (p,x)=0) {u : P → 𝓢'(E,ℂ)}
        (hu : SmoothSobolev N u) :
        SmoothSobolev N (fun p => smulLeftCLM ℂ (fun x => a (p,x)) (u p)) := by
    …

    Mentions: OAI.ElasticityRegularity.SmoothSobolev

47. lemma OAI.ElasticityPlanarDistribution.SmoothLocalSobolev.dhol line 693
48. theorem OAI.ElasticityPlanarDistribution.smooth_local_gain line 699

    Source documentation

    Actual smooth parameter-dependent elliptic gain for the planar system.

    theorem smooth_local_gain {Ω : Set ℂ} {s : ℝ}
        (a : n → n → ℂ → ℂ) (ha : ∀ i j, (a i j).HasTemperateGrowth)
        (c : P → ℂ) (hc : ContDiff ℝ (⊤ : ℕ∞) c)
        (u f : P → n → Dist)
        (heq : ∀ p i, LocalEqual Ω (dbar (u p i))
          (f p i+c p • ∑ j, smulLeftCLM ℂ (a i j) (u p j)))
        (hu : ∀ i, ElasticityRegularity.SmoothLocalSobolev Ω s (fun p => u p i))
        (hf : ∀ i, ElasticityRegularity.SmoothLocalSobolev Ω s (fun p => f p i)) :
        ∀ i, ElasticityRegularity.SmoothLocalSobolev Ω (s+1) (fun p => u p i) := by
    …

    Mentions: OAI.ElasticityPlanarDistribution.Dist, OAI.ElasticityPlanarDistribution.dbar, OAI.ElasticityRegularity.SmoothLocalSobolev

49. theorem OAI.ElasticityPlanarDistribution.smooth_local_all_orders line 718
50. theorem OAI.ElasticityRegularity.exists_bounded_continuous_embedding line 742

    Source documentation

    The continuous Sobolev embedding is a genuinely bounded operator, obtained from the actual Fourier representative and the closed graph theorem.

    theorem exists_bounded_continuous_embedding {s : ℝ} (hs : Module.finrank ℝ E < 2*s) :
        ∃ L : Lp ℂ 2 (volume : Measure E) →L[ℂ] BoundedContinuousFunction E ℂ,
          ∀ f, sobolevInjection s f=
            (((L f).memLp_top.toLp _ : Lp ℂ ∞ (volume : Measure E)) : 𝓢'(E,ℂ)) := by
    …

    Mentions: OAI.ElasticityRegularity.sobolevInjection

51. lemma OAI.ElasticityRegularity.SmoothSobolev.continuous_representative line 765
52. lemma OAI.ElasticityRegularity.SmoothSobolev.joint_continuous_representative line 773
53. def OAI.ElasticityRegularity.bcfToLinfty line 786
54. def OAI.ElasticityRegularity.bcfToDist line 796
55. lemma OAI.ElasticityRegularity.bcfToDist_apply line 798
56. lemma OAI.ElasticityRegularity.bcfToDist_injective line 800
57. lemma OAI.ElasticityRegularity.bcf_smooth_of_all_orders line 807
58. lemma OAI.ElasticityRegularity.bcf_derivative line 816

    Source documentation

    Distributional and classical derivatives agree for the actual bounded smooth representatives. A compact smooth multiplier makes every term Schwartz.

    lemma bcf_derivative (g h : BoundedContinuousFunction E ℂ)
        (hg : ContDiff ℝ (⊤ : ℕ∞) (g : E → ℂ))
        (hh : ContDiff ℝ (⊤ : ℕ∞) (h : E → ℂ)) (a x : E)
        (he : ∂_{a} (bcfToDist g)=bcfToDist h) :
        fderiv ℝ (g : E → ℂ) x a=h x := by
    …

    Mentions: OAI.ElasticityRegularity.bcfToDist

59. lemma OAI.ElasticityRegularity.bcf_family_spatial_smooth line 853
60. lemma OAI.ElasticityRegularity.bcf_parameter_derivative line 863
61. lemma OAI.ElasticityRegularity.bcf_spatial_derivative line 890

    Source documentation

    Actual spatial derivatives have smoothly parameter-dependent bounded representatives in every Sobolev order.

    lemma bcf_spatial_derivative (g : P → BoundedContinuousFunction E ℂ)
        (hu : ∀ n : ℕ, SmoothSobolev n (fun p => bcfToDist (g p))) (a : E) :
        ∃ h : P → BoundedContinuousFunction E ℂ,
          ContDiff ℝ (⊤ : ℕ∞) h ∧
          (∀ n : ℕ, SmoothSobolev n (fun p => bcfToDist (h p))) ∧
          ∀ p x, fderiv ℝ (g p : E → ℂ) x a=h p x := by
    …

    Mentions: OAI.ElasticityRegularity.SmoothSobolev, OAI.ElasticityRegularity.bcfToDist

62. lemma OAI.ElasticityRegularity.bcf_joint_hasFDerivAt line 914
63. theorem OAI.ElasticityRegularity.bcf_joint_smooth line 948

    Source documentation

    Strong smoothness in every Sobolev order yields actual joint smoothness, including mixed parameter and spatial derivatives.

    theorem bcf_joint_smooth (g : P → BoundedContinuousFunction E ℂ)
        (hg : ContDiff ℝ (⊤ : ℕ∞) g)
        (hu : ∀ n : ℕ, SmoothSobolev n (fun p => bcfToDist (g p))) :
        ContDiff ℝ (⊤ : ℕ∞) (fun q : P × E => g q.1 q.2) := by
    …

    Mentions: OAI.ElasticityRegularity.SmoothSobolev, OAI.ElasticityRegularity.bcfToDist

64. theorem OAI.ElasticityRegularity.SmoothSobolev.joint_smooth_representative line 976
65. theorem OAI.ElasticityRegularity.SmoothLocalSobolev.joint_schwartz_representative line 999

    Source documentation

    Joint smoothness on an arbitrary smaller fixed open set. The representative is an actual Schwartz function in space for every parameter.

    theorem SmoothLocalSobolev.joint_schwartz_representative {Ω Ω' : Set E}
        (u : P → 𝓢'(E,ℂ)) (hu : ∀ N : ℕ, SmoothLocalSobolev Ω N u)
        {g : E → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hc : HasCompactSupport g)
        (hs : tsupport g ⊆ Ω) (h1 : Set.EqOn g 1 Ω') :
        ∃ f : P → 𝓢(E,ℂ), ContDiff ℝ (⊤ : ℕ∞) (fun q : P × E => f q.1 q.2) ∧
          ∀ p, LocalEqual Ω' (u p) (f p : 𝓢'(E,ℂ)) := by
    …

    Mentions: OAI.ElasticityRegularity.SmoothLocalSobolev, OAI.ElasticityRegularity.LocalEqual

66. def OAI.ElasticityPlanar.schwartzDbar line 1027
67. lemma OAI.ElasticityPlanar.dbar_schwartz line 1028
68. lemma OAI.ElasticityPlanar.LocalEqual.dbar line 1033
69. lemma OAI.ElasticityPlanar.LocalEqual.coeff line 1037
70. theorem OAI.ElasticityPlanar.exists_planar_classical_solution line 1052

    Source documentation

    The actual matrix Cauchy--Riemann equation is solvable smoothly on every smaller open set. The unknown is produced by the supported estimate and Hilbert space duality, and the smooth solution is the same L2 solution almost everywhere. No pre-existing local or global frame is used.

    theorem exists_planar_classical_solution {S Ω Ω' : Set ℂ} (hS : IsCompact S)
        (hΩS : Ω ⊆ S) (hΩ' : IsOpen Ω') (hsub : Ω' ⊆ Ω)
        (a : n → n → ℂ → ℂ) (ha : ∀ i j, (a i j).HasTemperateGrowth)
        (f : n → 𝓢(ℂ,ℂ)) {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g)
        (hc : HasCompactSupport g) (hs : tsupport g ⊆ Ω) (h1 : Set.EqOn g 1 Ω') :
        ∃ w : Hilbert n, ∃ v : n → 𝓢(ℂ,ℂ),
          (∀ i, ∀ᵐ z ∂(volume : Measure ℂ), z ∈ Ω' → w i z=v i z) ∧
          ∀ i, Set.EqOn (fun z => schwartzDbar (v i) z+∑ j, a i j z*v j z) (f i) Ω' := by
    …

    Mentions: OAI.ElasticityPlanar.Hilbert, OAI.ElasticityPlanar.schwartzDbar

71. lemma OAI.ElasticityRegularity.SmoothSobolev.local_nat line 1113
72. lemma OAI.ElasticityRegularity.smoothSobolev_schwartz_const line 1119
73. theorem OAI.ElasticityPlanar.exists_classical_homotopy line 1131

    Source documentation

    The weak inverse along the entire coefficient homotopy has actual joint smooth classical representatives with the exact prescribed source. This is the linear PDE input to the frame homotopy, not an assumed family of invertible frames.

    theorem exists_classical_homotopy {S Ω Ω' : Set ℂ} (hS : IsCompact S)
        (hΩS : Ω ⊆ S) (hΩ' : IsOpen Ω') (hsub : Ω' ⊆ Ω)
        (a : n → n → ℂ → ℂ) (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j))
        (hac : ∀ i j, HasCompactSupport (a i j)) (f : n → 𝓢(ℂ,ℂ))
        {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g)
        (hc : HasCompactSupport g) (hs : tsupport g ⊆ Ω) (h1 : Set.EqOn g 1 Ω') :
        ∃ v : ℝ → n → 𝓢(ℂ,ℂ),
          (∀ i, ContDiff ℝ (⊤ : ℕ∞) (fun q : ℝ × ℂ => v q.1 i q.2)) ∧
          ∀ s i, Set.EqOn (fun z => schwartzDbar (v s i) z+∑ j, (s:ℂ)*a i j z*v s j z) (f i) Ω' := by
    …

    Mentions: OAI.ElasticityPlanar.schwartzDbar

74. lemma OAI.ElasticityRegularity.exists_schwartz_one_on_compact line 1210
75. theorem OAI.ElasticityRegularity.compact_smooth_sobolev line 1224

    Source documentation

    The actual Schwartz representatives of joint smooth uniform-compact-support families vary smoothly in every nonnegative Hilbert Sobolev norm.

    theorem compact_smooth_sobolev {K : Set E} (hK : IsCompact K)
        (a : P × E → ℂ) (ha : ContDiff ℝ (⊤ : ℕ∞) a)
        (hs : ∀ p x, x∉K → a (p,x)=0) :
        ∃ f : P → 𝓢(E,ℂ), (∀ p x, f p x=a (p,x)) ∧
          ∀ N : ℕ, SmoothSobolev N (fun p => (f p : 𝓢'(E,ℂ))) := by
    …

    Mentions: OAI.ElasticityRegularity.SmoothSobolev

76. lemma OAI.ElasticityRegularity.SmoothLocalSobolev.variable_nat line 1251
77. theorem OAI.ElasticityPlanarDistribution.smooth_variable_all_orders line 1271

    Source documentation

    The full variable-coefficient planar weak equation has strong smooth parameter regularity at every spatial order.

    theorem smooth_variable_all_orders {Ω S : Set ℂ} (hS : IsCompact S)
        (a : n → n → P × ℂ → ℂ) (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j))
        (hs : ∀ i j p z, z∉S → a i j (p,z)=0)
        (u f : P → n → Dist)
        (heq : ∀ p i, LocalEqual Ω (dbar (u p i))
          (f p i+∑ j, smulLeftCLM ℂ (fun z => a i j (p,z)) (u p j)))
        (hu : ∀ i, ElasticityRegularity.SmoothLocalSobolev Ω 0 (fun p => u p i))
        (hf : ∀ N : ℕ, ∀ i, ElasticityRegularity.SmoothLocalSobolev Ω N (fun p => f p i)) :
        ∀ N : ℕ, ∀ i, ElasticityRegularity.SmoothLocalSobolev Ω N (fun p => u p i) := by
    …

    Mentions: OAI.ElasticityPlanarDistribution.Dist, OAI.ElasticityPlanarDistribution.dbar, OAI.ElasticityRegularity.SmoothLocalSobolev

78. theorem OAI.ElasticityPlanar.exists_classical_variable line 1305

    Source documentation

    Actual smooth classical solutions for arbitrary joint smooth compactly supported planar coefficient and source families.

    theorem exists_classical_variable {S Ω Ω' K : Set ℂ} (hS : IsCompact S)
        (hΩS : Ω ⊆ S) (hΩ' : IsOpen Ω') (hsub : Ω' ⊆ Ω) (hK : IsCompact K)
        (a : n → n → P × ℂ → ℂ) (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j))
        (hac : ∀ i j p z, z∉K → a i j (p,z)=0)
        (f : n → P × ℂ → ℂ) (hf : ∀ i, ContDiff ℝ (⊤ : ℕ∞) (f i))
        (hfc : ∀ i p z, z∉K → f i (p,z)=0)
        {g : ℂ → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g)
        (hc : HasCompactSupport g) (hs : tsupport g ⊆ Ω) (h1 : Set.EqOn g 1 Ω') :
        ∃ v : P → n → 𝓢(ℂ,ℂ),
          (∀ i, ContDiff ℝ (⊤ : ℕ∞) (fun q : P × ℂ => v q.1 i q.2)) ∧
          ∀ p i, Set.EqOn (fun z => schwartzDbar (v p i) z+∑ j, a i j (p,z)*v p j z)
            (fun z => f i (p,z)) Ω' := by
    …

    Mentions: OAI.ElasticityPlanar.schwartzDbar