OAI/MathematicalPhysics/Elasticity/Supported.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ElasticityGraph.exists_coercive_left_inverse line 15

   Source documentation

   Orthogonal projection supplies a genuine bounded left inverse of a coercive Hilbert operator on all of the target space.

   theorem exists_coercive_left_inverse (A : E →L[ℂ] F) (C : ℝ) (hC : 0≤C)
       (hA : ∀ x, ‖x‖≤C*‖A x‖) :
       ∃ R : F →L[ℂ] E, R.comp A=ContinuousLinearMap.id ℂ E := by
   …

2. theorem OAI.ElasticityGraph.local_smooth_left_inverse line 44

   Source documentation

   A smooth local left inverse, with no surjectivity hypothesis.

   theorem local_smooth_left_inverse (A : P → E →L[ℂ] F)
       (hA : ContDiff ℝ (⊤ : ℕ∞) A) (p₀ : P) (C : ℝ) (hC : 0≤C)
       (hbound : ∀ x, ‖x‖≤C*‖A p₀ x‖) :
       ∃ (U : Set P) (R : P → F →L[ℂ] E), IsOpen U ∧ p₀∈U ∧
         ContDiffOn ℝ (⊤ : ℕ∞) R U ∧ ∀ p∈U, (R p).comp (A p)=ContinuousLinearMap.id ℂ E := by
   …

3. theorem OAI.ElasticityGraph.local_smooth_solution_of_dense line 81

   Source documentation

   Smooth dependence and existence at all parameters follow from existence on a dense set, using the actual local Hilbert left inverse.

   theorem local_smooth_solution_of_dense (A : P → E →L[ℂ] F)
       (hA : ContDiff ℝ (⊤ : ℕ∞) A) (f : P → F) (hf : ContDiff ℝ (⊤ : ℕ∞) f)
       {D : Set P} (hD : Dense D) (hex : ∀ p∈D, ∃ u, A p u=f p)
       (p₀ : P) (C : ℝ) (hC : 0≤C) (hbound : ∀ x, ‖x‖≤C*‖A p₀ x‖) :
       ∃ (U : Set P) (u : P → E), IsOpen U ∧ p₀∈U ∧
         ContDiffOn ℝ (⊤ : ℕ∞) u U ∧ ∀ p∈U, A p (u p)=f p := by
   …

4. abbrev OAI.ElasticityPlanar.GraphSpace line 109
5. def OAI.ElasticityPlanar.testGraph line 110
6. def OAI.ElasticityPlanar.closedGraph line 115
7. instance OAI.ElasticityPlanar.graphComplete line 118
8. def OAI.ElasticityPlanar.graphFirst line 122
9. def OAI.ElasticityPlanar.graphSecond line 125
10. theorem OAI.ElasticityPlanar.closed_graph_estimate line 130

    Source documentation

    The positive-commutator coercivity survives the actual graph closure.

    theorem closed_graph_estimate {S : Set ℂ} (hS : IsCompact S)
        (a : n → n → ℂ → ℂ) (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j)) :
        ∃ C : ℝ, 0<C ∧ ∀ u : closedGraph S a ha,
          ‖u‖≤C*‖graphSecond S a ha u‖ := by
    …

    Mentions: OAI.ElasticityPlanar.C, OAI.ElasticityPlanar.closedGraph, OAI.ElasticityPlanar.graphSecond

11. lemma OAI.ElasticityPlanar.L2_distribution line 157
12. lemma OAI.ElasticityPlanar.planarOperator_test line 159
13. theorem OAI.ElasticityPlanar.graph_equation line 174

    Source documentation

    Closing compact test graphs preserves the actual distributional operator.

    theorem graph_equation (S : Set ℂ) (a : n → n → ℂ → ℂ)
        (ha : ∀ i j, (a i j).HasTemperateGrowth)
        (u : closedGraph S a (fun i j => (ha i j).1)) (i : n) :
        planarOperator a i (graphFirst S a (fun i j => (ha i j).1) u)=
          entryInjection i (graphSecond S a (fun i j => (ha i j).1) u) := by
    …

    Mentions: OAI.ElasticityPlanar.closedGraph, OAI.ElasticityPlanar.planarOperator, OAI.ElasticityPlanar.graphFirst, OAI.ElasticityPlanar.entryInjection, OAI.ElasticityPlanar.graphSecond

14. lemma OAI.ElasticityPlanar.test_support_distribution line 187
15. theorem OAI.ElasticityPlanar.graph_support line 203

    Source documentation

    Graph closure retains support, in the literal distributional sense.

    theorem graph_support (S : Set ℂ) (a : n → n → ℂ → ℂ)
        (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j))
        (u : closedGraph S a ha) (i : n) :
        LocalEqual Sᶜ (entryInjection i (graphFirst S a ha u)) 0 := by
    …

    Mentions: OAI.ElasticityPlanar.closedGraph, OAI.ElasticityPlanar.entryInjection, OAI.ElasticityPlanar.graphFirst

16. lemma OAI.ElasticityPlanar.shifted_graph_equation line 222
17. lemma OAI.ElasticityPlanar.graph_test_solution line 238
18. lemma OAI.ElasticityPlanar.local_graph_solution line 256
19. theorem OAI.ElasticityPlanar.local_supported_of_dense_tests line 270

    Source documentation

    A local smooth supported solution family, derived from compact-test graph solvability on a dense set. No range-surjectivity assumption is required.

    theorem local_supported_of_dense_tests {S K : Set ℂ} (hS : IsCompact 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)
        (f : P → Hilbert n) (hf : ContDiff ℝ (⊤ : ℕ∞) f) {D : Set P} (hD : Dense D)
        (hex : ∀ p∈D, ∃ v : n → Test, (∀ i, tsupport (v i : ℂ → ℂ)⊆S) ∧
          ∀ i, planarOperator (fun i j z => a i j (p,z)) i (embed v)=entryInjection i (f p))
        (p₀ : P) :
        ∃ (U : Set P) (u : P → Hilbert n), IsOpen U ∧ p₀∈U ∧
          ContDiffOn ℝ (⊤ : ℕ∞) u U ∧ ∀ p∈U, ∀ i,
            planarOperator (fun i j z => a i j (p,z)) i (u p)=entryInjection i (f p) ∧
            LocalEqual Sᶜ (entryInjection i (u p)) 0 := by
    …

    Mentions: OAI.ElasticityPlanar.Hilbert, OAI.ElasticityPlanar.Test, OAI.ElasticityPlanar.planarOperator, OAI.ElasticityPlanar.embed, OAI.ElasticityPlanar.entryInjection

20. lemma OAI.ElasticityPlanar.supported_smooth_test line 314
21. lemma OAI.ElasticityPlanar.operator_all_orders line 371
22. theorem OAI.ElasticityPlanar.supported_weak_is_test line 393

    Source documentation

    Smooth forcing upgrades every supported weak L2 solution to an actual compact smooth test vector, by the established elliptic regularity and support identity.

    theorem supported_weak_is_test {S : Set ℂ} (hS : IsCompact S)
        (a : n → n → ℂ → ℂ) (ha : ∀ i j, (a i j).HasTemperateGrowth)
        (w : Hilbert n) (f : n → 𝓢(ℂ,ℂ))
        (he : ∀ i, planarOperator a i w=(f i : 𝓢'(ℂ,ℂ)))
        (hs : ∀ i, LocalEqual Sᶜ (entryInjection i w) 0) :
        ∃ v : n → Test, embed v=w ∧ ∀ i, tsupport (v i : ℂ → ℂ)⊆S := by
    …

    Mentions: OAI.ElasticityPlanar.Hilbert, OAI.ElasticityPlanar.planarOperator, OAI.ElasticityPlanar.entryInjection, OAI.ElasticityPlanar.Test, OAI.ElasticityPlanar.embed

23. theorem OAI.ElasticityPlanar.supported_weak_kernel line 406

    Source documentation

    Compact support gives uniqueness for the genuine weak transport operator.

    theorem supported_weak_kernel {S : Set ℂ} (hS : IsCompact S)
        (a : n → n → ℂ → ℂ) (ha : ∀ i j, (a i j).HasTemperateGrowth)
        (w : Hilbert n) (he : ∀ i, planarOperator a i w=0)
        (hs : ∀ i, LocalEqual Sᶜ (entryInjection i w) 0) : w=0 := by
    …

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

24. lemma OAI.ElasticityPlanar.compact_smooth_source line 429
25. theorem OAI.ElasticityPlanar.global_supported_of_dense line 453

    Source documentation

    Dense-parameter supported weak solvability extends to all parameters in the actual L2/distribution spaces, and the solution varies strongly smoothly.

    theorem global_supported_of_dense {S K : Set ℂ} (hS : IsCompact 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)
        (F : P → n → 𝓢(ℂ,ℂ)) (f : P → Hilbert n)
        (hf : ContDiff ℝ (⊤ : ℕ∞) f) (hFe : ∀ p i, entryInjection i (f p)=(F p i : 𝓢'(ℂ,ℂ)))
        {D : Set P} (hD : Dense D)
        (hex : ∀ p∈D, ∃ w : Hilbert n, ∀ i,
          planarOperator (fun i j z => a i j (p,z)) i w=entryInjection i (f p) ∧
          LocalEqual Sᶜ (entryInjection i w) 0) :
        ∃ u : P → Hilbert n, ContDiff ℝ (⊤ : ℕ∞) u ∧ ∀ p i,
          planarOperator (fun i j z => a i j (p,z)) i (u p)=entryInjection i (f p) ∧
          LocalEqual Sᶜ (entryInjection i (u p)) 0 := by
    …

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

26. lemma OAI.ElasticityPlanar.smooth_operator_all_orders line 505
27. lemma OAI.ElasticityPlanar.supported_smooth_test_family line 543
28. theorem OAI.ElasticityPlanar.supported_parameter_inversion line 609

    Source documentation

    The dense-parameter assertion uses genuine weak solutions, not an assumed smooth selection. Compact support and the elliptic estimate construct the unique jointly smooth selection.

    theorem supported_parameter_inversion {S K : Set ℂ} (hS : IsCompact 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)
        (f : n → P × ℂ → ℂ) (hf : ∀ i, ContDiff ℝ (⊤ : ℕ∞) (f i))
        (hfs : ∀ i p z, z∉K → f i (p,z)=0)
        {D : Set P} (hD : Dense D)
        (hex : ∀ p∈D, ∃ w : Hilbert n, ∀ i,
          planarOperator (fun i j z => a i j (p,z)) i w=
            (toSchwartz ⟨fun z => f i (p,z),⟨(hf i).comp (contDiff_const.prodMk contDiff_id),
              compact_slice hK (f i) (hfs i) p⟩⟩ : 𝓢'(ℂ,ℂ)) ∧
          LocalEqual Sᶜ (entryInjection i w) 0) :
        ∃ v : P → n → Test,
    …

    Mentions: OAI.ElasticityPlanar.Hilbert, OAI.ElasticityPlanar.planarOperator, OAI.ElasticityPlanar.toSchwartz, OAI.ElasticityPlanar.entryInjection, OAI.ElasticityPlanar.Test

29. lemma OAI.ElasticityPlanar.supported_weak_unique line 666
30. lemma OAI.ElasticityGeneralSlicing.tests_determine_supported line 688
31. lemma OAI.ElasticityGeneralSlicing.supported_local_zero line 725
32. lemma OAI.ElasticityGeneralSlicing.supported_slice line 739

    Source documentation

    Compact support passes through Fubini and through the chosen L2 representative.

    lemma supported_slice (S : Set ℂ) (u : P × ℂ → ℂ)
        (hu : MemLp u 2 volume) (hs : ∀ᵐ q : P × ℂ, q.2∉S → u q=0) :
        ∀ᵐ t : P, ∀ᵐ z : ℂ, z∉S → sliceLp u t z=0 := by
    …

    Mentions: OAI.ElasticityGeneralSlicing.sliceLp

33. theorem OAI.ElasticityGeneralSlicing.cylinder_supported_slices line 751

    Source documentation

    The slicing result is an actual global planar distribution equation, not merely equality on a selected family of test functions.

    theorem cylinder_supported_slices (S : Set ℂ) (hS : IsCompact S)
        (u w : Lp ℂ 2 (volume : Measure (P × ℂ)))
        (hu : Integrable (u : P × ℂ → ℂ)) (hw : Integrable (w : P × ℂ → ℂ))
        (hsu : ∀ᵐ q : P × ℂ, q.2∉S → u q=0) (hsw : ∀ᵐ q : P × ℂ, q.2∉S → w q=0)
        (he : ∂_{((0:P),(1:ℂ))} (u : 𝓢'(P × ℂ,ℂ))+
          Complex.I • ∂_{((0:P),Complex.I)} (u : 𝓢'(P × ℂ,ℂ))+(w : 𝓢'(P × ℂ,ℂ))=0) :
        ∀ᵐ t : P,
          dbar (sliceLp u t : Dist)+(sliceLp w t : Dist)=0 ∧
          LocalEqual Sᶜ (sliceLp u t : Dist) 0 := by
    …

    Mentions: OAI.ElasticityGeneralSlicing.sliceLp

34. lemma OAI.ElasticityGeneralSlicing.sliced_coefficients line 787
35. theorem OAI.ElasticityGeneralSlicing.coupled_slice_equations line 820

    Source documentation

    Genuine cylinder weak solutions give supported weak planar solutions on a single full-measure, hence dense, set of transverse parameters.

    theorem coupled_slice_equations (S K : Set ℂ) (hS : IsCompact S) (hK : IsCompact K)
        (a : n → n → P × ℂ → ℂ) (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j))
        (hs : ∀ i j t z,z∉K → a i j (t,z)=0)
        (f : n → P × ℂ → ℂ) (hf : ∀ i,ContDiff ℝ (⊤ : ℕ∞) (f i))
        (hfs : ∀ i t z,z∉K → f i (t,z)=0)
        (u w : n → Lp ℂ 2 (volume : Measure (P × ℂ)))
        (hu : ∀ i,Integrable (u i : P × ℂ → ℂ)) (hw : ∀ i,Integrable (w i : P × ℂ → ℂ))
        (hsu : ∀ i,∀ᵐ q : P × ℂ,q.2∉S → u i q=0)
        (hsw : ∀ i,∀ᵐ q : P × ℂ,q.2∉S → w i q=0)
        (hc : ∀ i,∀ᵐ q : P × ℂ,w i q=∑ j,a i j q*u j q-f i q)
        (he : ∀ i, ∂_{((0:P),(1:ℂ))} (u i : 𝓢'(P × ℂ,ℂ))+
          Complex.I • ∂_{((0:P),Complex.I)} (u i : 𝓢'(P × ℂ,ℂ))+(w i : 𝓢'(P × ℂ,ℂ))=0) :
    …

36. theorem OAI.ElasticityGeneralSlicing.smooth_supported_of_cylinder line 878

    Source documentation

    Completion of the almost-every-plane to every-plane step. No smooth weak representative or nowhere-exceptional slicing has been assumed.

    theorem smooth_supported_of_cylinder (S K : Set ℂ) (hS : IsCompact S) (hK : IsCompact K)
        (a : n → n → P × ℂ → ℂ) (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j))
        (hs : ∀ i j t z,z∉K → a i j (t,z)=0)
        (f : n → P × ℂ → ℂ) (hf : ∀ i,ContDiff ℝ (⊤ : ℕ∞) (f i))
        (hfs : ∀ i t z,z∉K → f i (t,z)=0)
        (u w : n → Lp ℂ 2 (volume : Measure (P × ℂ)))
        (hu : ∀ i,Integrable (u i : P × ℂ → ℂ)) (hw : ∀ i,Integrable (w i : P × ℂ → ℂ))
        (hsu : ∀ i,∀ᵐ q : P × ℂ,q.2∉S → u i q=0)
        (hsw : ∀ i,∀ᵐ q : P × ℂ,q.2∉S → w i q=0)
        (hc : ∀ i,∀ᵐ q : P × ℂ,w i q=∑ j,a i j q*u j q-f i q)
        (he : ∀ i, ∂_{((0:P),(1:ℂ))} (u i : 𝓢'(P × ℂ,ℂ))+
          Complex.I • ∂_{((0:P),Complex.I)} (u i : 𝓢'(P × ℂ,ℂ))+(w i : 𝓢'(P × ℂ,ℂ))=0) :
    …

37. lemma OAI.ElasticityGeneralSlicing.classical_planar_distribution line 905
38. theorem OAI.ElasticityGeneralSlicing.smooth_cylinder_representative line 928

    Source documentation

    The jointly smooth solution is the actual weak cylinder solution, not an unrelated branch. Supported uniqueness identifies it on almost every slice.

    theorem smooth_cylinder_representative (S K : Set ℂ) (hS : IsCompact S) (hK : IsCompact K)
        (a : n → n → P × ℂ → ℂ) (ha : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (a i j))
        (hs : ∀ i j t z,z∉K → a i j (t,z)=0)
        (f : n → P × ℂ → ℂ) (hf : ∀ i,ContDiff ℝ (⊤ : ℕ∞) (f i))
        (hfs : ∀ i t z,z∉K → f i (t,z)=0)
        (u w : n → Lp ℂ 2 (volume : Measure (P × ℂ)))
        (hu : ∀ i,Integrable (u i : P × ℂ → ℂ)) (hw : ∀ i,Integrable (w i : P × ℂ → ℂ))
        (hsu : ∀ i,∀ᵐ q : P × ℂ,q.2∉S → u i q=0)
        (hsw : ∀ i,∀ᵐ q : P × ℂ,q.2∉S → w i q=0)
        (hc : ∀ i,∀ᵐ q : P × ℂ,w i q=∑ j,a i j q*u j q-f i q)
        (he : ∀ i, ∂_{((0:P),(1:ℂ))} (u i : 𝓢'(P × ℂ,ℂ))+
          Complex.I • ∂_{((0:P),Complex.I)} (u i : 𝓢'(P × ℂ,ℂ))+(w i : 𝓢'(P × ℂ,ℂ))=0) :
    …