OAI/MathematicalPhysics/Elasticity/LocalRegularity.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElasticityRegularity.LocalEqual line 19
2. lemma OAI.ElasticityRegularity.LocalEqual.refl line 23
3. lemma OAI.ElasticityRegularity.LocalEqual.symm line 24
4. lemma OAI.ElasticityRegularity.LocalEqual.trans line 25
5. lemma OAI.ElasticityRegularity.LocalEqual.add line 27
6. lemma OAI.ElasticityRegularity.LocalEqual.sub line 30
7. lemma OAI.ElasticityRegularity.LocalEqual.smul line 33
8. lemma OAI.ElasticityRegularity.LocalEqual.sum line 36
9. lemma OAI.ElasticityRegularity.LocalEqual.derivative line 41
10. lemma OAI.ElasticityRegularity.LocalEqual.cutoff line 50
11. lemma OAI.ElasticityRegularity.LocalEqual.localSobolev line 61
12. lemma OAI.ElasticityRegularity.LocalSobolev.add line 69
13. lemma OAI.ElasticityRegularity.LocalSobolev.sub line 73
14. lemma OAI.ElasticityRegularity.LocalSobolev.smul line 77
15. lemma OAI.ElasticityRegularity.LocalSobolev.sum line 81
16. lemma OAI.ElasticityRegularity.LocalSobolev.coeff line 86
17. lemma OAI.ElasticityRegularity.LocalSobolev.derivative line 91
18. lemma OAI.ElasticityRegularity.local_laplacian_gain_basis line 96
19. lemma OAI.ElasticityRegularity.schwartz_dist_injective line 121
20. lemma OAI.ElasticityRegularity.distribution_schwartz_product line 129
21. lemma OAI.ElasticityRegularity.LocalEqual.cutoff_one line 139
22. lemma OAI.ElasticityRegularity.LocalEqual.schwartz_eqOn line 152
23. lemma OAI.ElasticityRegularity.smooth_Linfty_product line 179
24. theorem OAI.ElasticityRegularity.local_schwartz_representative line 196

    Source documentation

    Interior cutoff regularity yields an actual Schwartz representative on the smaller open set; this is what is needed to construct physical smooth CGO solutions on a ball from an L2 weak solution on a larger ball.

    theorem local_schwartz_representative {Ω Ω' : Set E} (u : 𝓢'(E,ℂ))
        (hu : ∀ N : ℕ, LocalSobolev Ω N u) {g : E → ℂ}
        (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hc : HasCompactSupport g)
        (hs : tsupport g ⊆ Ω) (h1 : Set.EqOn g 1 Ω') :
        ∃ v : 𝓢(E,ℂ), LocalEqual Ω' u (v : 𝓢'(E,ℂ)) := by
    …

    Mentions: OAI.ElasticityRegularity.LocalSobolev, OAI.ElasticityRegularity.LocalEqual

25. lemma OAI.ElasticityRegularity.LocalEqual.lp_ae line 215
26. theorem OAI.ElasticityRegularity.local_schwartz_l2_representative line 251

    Source documentation

    The smooth local representative really is the original L2 function almost everywhere, so the HB solution's L2 estimate is not lost in regularization.

    theorem local_schwartz_l2_representative {Ω Ω' : Set E} (hΩ' : IsOpen Ω')
        (u : Lp ℂ 2 (volume : Measure E))
        (hu : ∀ N : ℕ, LocalSobolev Ω N (u : 𝓢'(E,ℂ))) {g : E → ℂ}
        (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hc : HasCompactSupport g)
        (hs : tsupport g ⊆ Ω) (h1 : Set.EqOn g 1 Ω') :
        ∃ v : 𝓢(E,ℂ), LocalEqual Ω' (u : 𝓢'(E,ℂ)) (v : 𝓢'(E,ℂ)) ∧
          ∀ᵐ x ∂(volume : Measure E), x ∈ Ω' → u x=v x := by
    …

    Mentions: OAI.ElasticityRegularity.LocalSobolev, OAI.ElasticityRegularity.LocalEqual

27. lemma OAI.ElasticityDistribution.coe_schwartz_add line 272
28. lemma OAI.ElasticityDistribution.coe_schwartz_smul line 273
29. lemma OAI.ElasticityDistribution.coe_schwartz_sum line 274
30. lemma OAI.ElasticityDistribution.sd_schwartz line 276
31. lemma OAI.ElasticityDistribution.coeff_schwartz line 281
32. lemma OAI.ElasticityDistribution.divd_schwartz line 283
33. lemma OAI.ElasticityDistribution.phys_schwartz line 287
34. lemma OAI.ElasticityDistribution.LocalEq.physical line 292
35. theorem OAI.ElasticityDistribution.classical_representative line 300

    Source documentation

    A genuinely classical physical solution on an interior open set is obtained from the actual weak solution, and represents that same L2 unknown there.

    theorem classical_representative {Ω Ω' : Set X} (hΩ' : IsOpen Ω') (hsub : Ω' ⊆ Ω)
        (z : Fin 3 → ℂ) (lam m n o : Coeff) (hn : n*m=1) (ho : o*(lam+m+m)=1)
        (w : ElasticityPhysicalDual.H) (F : Fin 3 → S)
        (heq : ∀ i, LocalEq Ω (phys z lam m (fun j => (w j : Dist)) i) (F i : Dist))
        {g : X → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hc : HasCompactSupport g)
        (hs : tsupport g ⊆ Ω) (h1 : Set.EqOn g 1 Ω') :
        ∃ v : Fin 3 → S, (∀ i, ∀ᵐ x ∂(volume : Measure X), x ∈ Ω' → w i x=v i x) ∧
          ∀ i, Set.EqOn (physical z (eval lam) (eval m) v i : X → ℂ) (F i : X → ℂ) Ω' := by
    …

    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityPhysicalDual.H, OAI.ElasticityDistribution.S, OAI.ElasticityDistribution.LocalEq, OAI.ElasticityDistribution.phys, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.eval