OAI/MathematicalPhysics/Elasticity/PhysicalCGO.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElasticityAugmented.smoothOfReal line 13
2. lemma OAI.ElasticityAugmented.smoothOfReal_apply line 15
3. lemma OAI.ElasticityAugmented.coord_ofReal line 17
4. lemma OAI.ElasticityAugmented.recovery_basis line 21
5. lemma OAI.ElasticityAugmented.coord_ofReal_grad line 23
6. def OAI.ElasticityAugmented.positiveRoot line 28
7. lemma OAI.ElasticityAugmented.positiveRoot_nonzero line 30
8. lemma OAI.ElasticityAugmented.positiveRoot_square line 33
9. def OAI.ElasticityAugmented.smoothLog line 41
10. lemma OAI.ElasticityAugmented.coord_real_log line 43
11. lemma OAI.ElasticityAugmented.direction_real_log line 55
12. lemma OAI.ElasticityAugmented.logarithmicGrad_root line 64
13. lemma OAI.ElasticityAugmented.ofReal_direction line 86
14. lemma OAI.ElasticityAugmented.smoothOfReal_add line 91
15. lemma OAI.ElasticityAugmented.smoothLog_div line 96
16. lemma OAI.ElasticityAugmented.real_sum_nonzero line 104
17. lemma OAI.ElasticityAugmented.direction_sub line 110
18. lemma OAI.ElasticityAugmented.transportT_real line 114
19. lemma OAI.ElasticityAugmented.grad_contDiff line 137
20. lemma OAI.ElasticityAugmented.coord_real_grad line 140
21. lemma OAI.ElasticityAugmented.direction_coord_real line 146
22. lemma OAI.ElasticityAugmented.thetaGamma_real line 151
23. lemma OAI.ElasticityAugmented.transportQ_real line 157
24. lemma OAI.ElasticityAugmented.real_k_positive line 186
25. lemma OAI.ElasticityAugmented.real_longitudinal_positive line 188
26. theorem OAI.ElasticityAugmented.exists_real_physical_series line 193

    Source documentation

    Actual real strongly convex Lamé pairs develop to a full independent physical amplitude frame and all its compatible recursion orders.

    theorem exists_real_physical_series {U : Set X} (hU : IsOpen U) (hC : IsCompact (closure U))
        (θ : Fin 3 → ℂ) (hθ : ∑ i,θ i*θ i=0) (hne : θ≠0)
        (lam m : X → ℝ) (hl : ContDiff ℝ (⊤ : ℕ∞) lam) (hm : ContDiff ℝ (⊤ : ℕ∞) m)
        (hp : ∀ x,0 < m x ∧ 0<3*lam x+2*m x) :
        let l := smoothOfReal lam hl
    …

    Mentions: OAI.ElasticityAugmented.X, OAI.ElasticityAugmented.smoothOfReal

27. theorem OAI.Elasticity.extended_dn_amplitude_transfer line 241

    Source documentation

    Actual DN equality yields a shifted physical solution with a compact amplitude difference. This uses the common-exterior coefficients from the boundary reduction; it does not assume normalized-system transfer. The two cutoffs are ordinary compact smooth cutoffs on nested open domains.

    theorem extended_dn_amplitude_transfer {Ω B B' : Set X}
        (hΩ : IsOpen Ω) (hOB : Bornology.IsBounded Ω) (hB : IsOpen B)
        (hBB : Bornology.IsBounded B) (hB' : IsOpen B') (hsub : B'⊆B) (hcl : closure Ω⊆B')
        (lam m : Fin 2 → X → ℝ)
        (hl : ∀ q,ContDiff ℝ (⊤ : ℕ∞) (lam q)) (hm : ∀ q,ContDiff ℝ (⊤ : ℕ∞) (m q))
        (hp : ∀ q x,0 < m q x ∧ 0<3*lam q x+2*m q x)
        (hcll : ∀ q,ExteriorConstant (smoothOfReal (lam q) (hl q)))
        (hclm : ∀ q,ExteriorConstant (smoothOfReal (m q) (hm q)))
        (he : ∀ x∉Ω,lam 0 x=lam 1 x ∧ m 0 x=m 1 x)
        (hDN : DN Ω (lam 0) (m 0)=DN Ω (lam 1) (m 1))
        (χ g : Smooth) (hcχ : HasCompactSupport (χ : X → ℂ))
        (hc : HasCompactSupport (g : X → ℂ)) (hs : tsupport (g : X → ℂ)⊆B)
    …

    Mentions: OAI.Elasticity.X, OAI.Elasticity.DN

28. theorem OAI.Elasticity.extended_dn_compact_comparison line 304

    Source documentation

    The actual physical DN equality gives the uniform compact comparison bound. The Cauchy-data transfer, normalized forcing, and coefficient bounds are all proved dependencies. This theorem still starts at the common-exterior stage; it does not replace the missing original-boundary jet determination.

    theorem extended_dn_compact_comparison {Ω B B' : Set X}
        (hΩ : IsOpen Ω) (hOB : Bornology.IsBounded Ω) (hB : IsOpen B)
        (hBB : Bornology.IsBounded B) (hB' : IsOpen B') (hsub : B'⊆B) (hcl : closure Ω⊆B')
        (R : ℝ) (hR : 1≤R) (hKR : closure Ω⊆Metric.closedBall 0 R)
        (α β : X) (hα : α≠0)
        (lam m : Fin 2 → X → ℝ)
        (hl : ∀ q,ContDiff ℝ (⊤ : ℕ∞) (lam q)) (hm : ∀ q,ContDiff ℝ (⊤ : ℕ∞) (m q))
        (hp : ∀ q x,0 < m q x ∧ 0<3*lam q x+2*m q x)
        (hcll : ∀ q,ExteriorConstant (smoothOfReal (lam q) (hl q)))
        (hclm : ∀ q,ExteriorConstant (smoothOfReal (m q) (hm q)))
        (he : ∀ x∉Ω,lam 0 x=lam 1 x ∧ m 0 x=m 1 x)
        (hDN : DN Ω (lam 0) (m 0)=DN Ω (lam 1) (m 1))
    …

    Mentions: OAI.Elasticity.X, OAI.Elasticity.DN

29. lemma OAI.ElasticityRegularity.sobolevInjection_zero line 354
30. theorem OAI.ElasticityRegularity.standard_H1_controls_semiclassical line 362

    Source documentation

    A standard Sobolev H1 representative controls the actual semiclassical Fourier norm uniformly for h in (0,1]. The two Bessel conventions are not identified: this follows from their concrete L2 derivative realizations.

    theorem standard_H1_controls_semiclassical :
        ∃ C : ℝ,0<C ∧ ∀ h : ℝ,0≤h → h≤1 → ∀ f : S,
          ∀ q : Lp ℂ 2 (volume : Measure X),sobolevInjection 1 q=(f : 𝓢'(X,ℂ)) →
            norm2 (J h 1 f)≤C*‖q‖ := by
    …

    Mentions: OAI.ElasticityRegularity.sobolevInjection

31. theorem OAI.ElasticityRegularity.local_standard_H1_controls_semiclassical line 415

    Source documentation

    The same uniform bound after a compact cutoff, when only a local standard-H1 representative is available. This is the localization needed for the actual augmented CGO corrections.

    theorem local_standard_H1_controls_semiclassical {U : Set X} {g : X → ℂ}
        (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hc : HasCompactSupport g) (hs : tsupport g⊆U) :
        ∃ C : ℝ,0<C ∧ ∀ h : ℝ,0≤h → h≤1 → ∀ f : S,
          ∀ q : Lp ℂ 2 (volume : Measure X),
          LocalEqual U (sobolevInjection 1 q) (f : 𝓢'(X,ℂ)) →
            norm2 (J h 1 (mult g f))≤C*‖q‖ := by
    …

    Mentions: OAI.ElasticityRegularity.LocalEqual, OAI.ElasticityRegularity.sobolevInjection

32. theorem OAI.ElasticityCGO.physical_cgo_from_recursion line 454

    Source documentation

    A genuinely compatible finite amplitude series gives exact smooth physical CGO fields. The correction is the same estimated L2 solution, and its full physical divergence is H1-small. Neither a physical-solvability statement nor convergence of a formal infinite series is assumed.

    theorem physical_cgo_from_recursion (R : ℝ) (hR : 1≤R)
        (Ω U : Set X) (hΩ : Ω⊆Metric.closedBall 0 R) (hU : IsOpen U) (hsub : U⊆Ω)
        (α β : X) (hα : α≠0)
        (hθ : ∑ i,((α i : ℂ)+Complex.I*(β i : ℂ))*((α i : ℂ)+Complex.I*(β i : ℂ))=0)
        (lam m : Smooth) (hl : ExteriorConstant lam) (hm : ExteriorConstant m)
        (hrl : ∀ x,star ((lam : X → ℂ) x)=(lam : X → ℂ) x)
        (hrm : ∀ x,star ((m : X → ℂ) x)=(m : X → ℂ) x)
        (hm0 : ∀ x,(m : X → ℂ) x≠0)
        (he0 : ∀ x,((lam+m+m : Smooth) : X → ℂ) x≠0)
        (χ : Fin 5 → X → ℂ) (hχ : ∀ i, ContDiff ℝ (⊤ : ℕ∞) (χ i))
        (hcχ : ∀ i,HasCompactSupport (χ i))
        (hnest : ∀ i : Fin 4,EqOn (χ i.succ) 1 (tsupport (χ i.castSucc)))
    …

33. def OAI.ElasticityCGO.fiveCutoff line 501
34. lemma OAI.ElasticityCGO.fiveCutoff_smooth line 503
35. lemma OAI.ElasticityCGO.fiveCutoff_compact line 506
36. lemma OAI.ElasticityCGO.fiveCutoff_support line 509
37. lemma OAI.ElasticityCGO.fiveCutoff_one line 517
38. lemma OAI.ElasticityCGO.fiveCutoff_nested line 522
39. lemma OAI.ElasticityCGO.fiveCutoff_inside line 529
40. lemma OAI.ElasticityCGO.fiveCutoff_initial line 537
41. def OAI.ElasticityCGO.PhysicalColumn line 556

    Source documentation

    Quantified actual physical CGO corrections on the ball, with the full physical divergence in H1. This is a conclusion, never an input assumption.

    def PhysicalColumn (R : ℝ) (hR : 1≤R) (α β : X) (lam m : Smooth)
        (a : ℕ → Amplitude Smooth) : Prop :=
    …

42. theorem OAI.ElasticityCGO.physical_column_of_recursion line 569
43. theorem OAI.ElasticityCGO.exists_real_physical_cgo_frame line 592

    Source documentation

    A full genuine rank-three constrained frame of actual physical CGO columns for every smooth, constant-exterior, strongly convex real Lamé pair. The amplitudes and all corrections are constructed, not postulated.

    theorem exists_real_physical_cgo_frame (R : ℝ) (hR : 1≤R) (α β : X) (hα : α≠0)
        (hθ : ∑ i,((α i : ℂ)+Complex.I*(β i : ℂ))*((α i : ℂ)+Complex.I*(β i : ℂ))=0)
        (lam m : X → ℝ) (hl : ContDiff ℝ (⊤ : ℕ∞) lam) (hm : ContDiff ℝ (⊤ : ℕ∞) m)
        (hp : ∀ x,0 < m x ∧ 0<3*lam x+2*m x)
        (hcl : ExteriorConstant (smoothOfReal lam hl)) (hcm : ExteriorConstant (smoothOfReal m hm)) :
        let θ := fun i => (α i : ℂ)+Complex.I*(β i : ℂ)
    …

44. def OAI.ElasticityCGO.cgoField line 642
45. theorem OAI.ElasticityCGO.cgoField_apply_on line 649
46. theorem OAI.ElasticityCGO.physical_column_realization line 663

    Source documentation

    Realization of the constructed physical column by a literal exponential solution of the original (not augmented) elasticity equation.

    theorem physical_column_realization (R : ℝ) (hR : 1≤R) (α β : X) (lam m : Smooth)
        (hl : ExteriorConstant lam) (hm : ExteriorConstant m)
        (a : ℕ → Amplitude Smooth) (ha : PhysicalColumn R hR α β lam m a) :
        ∃ C h₀ : ℝ,0<C ∧ 0<h₀ ∧ ∀ h : ℝ,0<h → h≤h₀ →
          ∃ w : ElasticityPhysicalDual.H,∃ q : HV,∃ v : Fin 3 → S,
            (∀ i,∀ᵐ x ∂(volume : Measure X),x∈Metric.ball 0 R → w i x=v i x) ∧
            (∀ i,EqOn (physical 0 lam m (cgoField R hR h α β a v) i : X → ℂ) 0 (Metric.ball 0 R)) ∧
            (∀ i,sobolevInjection 1 (q i)=smulLeftCLM ℂ (fiveCutoff R hR 0)
              ((Fin.cons (divd (phase h α β) (fun j => (w j : Dist)))
                (fun j => (w j : Dist)) : Fin 4 → Dist) i)) ∧
            ‖w‖≤C*h^7 ∧ ‖q‖≤C*h := by
    …

    Mentions: OAI.ElasticityCGO.PhysicalColumn, OAI.ElasticityPhysicalDual.H, OAI.ElasticityCGO.S, OAI.ElasticityCGO.cgoField, OAI.ElasticityCGO.fiveCutoff

47. lemma OAI.ElasticityCGO.local_lp_schwartz_of_ae line 691
48. lemma OAI.ElasticityCGO.actual_augmented_local_representative line 707

    Source documentation

    The local standard-H1 representative controls the SAME physical correction and its actual shifted divergence.

    lemma actual_augmented_local_representative {U : Set X} (z : Fin 3 → ℂ)
        (χ : X → ℂ) (hχ : χ.HasTemperateGrowth) (h1 : EqOn χ 1 U)
        (w : ElasticityPhysicalDual.H) (q : HV) (v : Fin 3 → S)
        (hv : ∀ i,∀ᵐ x ∂(volume : Measure X),x∈U → w i x=v i x)
        (hq : ∀ i,sobolevInjection 1 (q i)=smulLeftCLM ℂ χ
          ((Fin.cons (divd z (fun j => (w j : Dist))) (fun j => (w j : Dist)) : Fin 4 → Dist) i)) :
        ∀ i,LocalEqual U (sobolevInjection 1 (q i)) (physicalAug z v i : Dist) := by
    …

    Mentions: OAI.ElasticityPhysicalDual.H, OAI.ElasticityCGO.S

49. theorem OAI.ElasticityCGO.actual_augmented_cutoff_bound line 725

    Source documentation

    Uniform compactly localized augmented correction bound; the scalar component is not independent of the displacement.

    theorem actual_augmented_cutoff_bound {U : Set X} {g : X → ℂ}
        (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hc : HasCompactSupport g) (hs : tsupport g⊆U) :
        ∃ C : ℝ,0<C ∧ ∀ h : ℝ,0≤h → h≤1 → ∀ z : Fin 3 → ℂ,
          ∀ χ : X → ℂ,χ.HasTemperateGrowth → EqOn χ 1 U →
          ∀ w : ElasticityPhysicalDual.H,∀ q : HV,∀ v : Fin 3 → S,
          (∀ i,∀ᵐ x ∂(volume : Measure X),x∈U → w i x=v i x) →
          (∀ i,sobolevInjection 1 (q i)=smulLeftCLM ℂ χ
            ((Fin.cons (divd z (fun j => (w j : Dist))) (fun j => (w j : Dist)) : Fin 4 → Dist) i)) →
          sobNorm h 1 (fun i => mult g (physicalAug z v i))≤C*‖q‖ := by
    …

    Mentions: OAI.ElasticityPhysicalDual.H, OAI.ElasticityCGO.S

50. lemma OAI.ElasticityCGO.divShift_mult line 746
51. theorem OAI.ElasticityCGO.cut_actual_augmented_bound line 767

    Source documentation

    Cutting off the displacement itself retains a uniformly controlled ACTUAL augmented field. The derivative of the cutoff has no phase loss.

    theorem cut_actual_augmented_bound {U : Set X} {g : X → ℂ}
        (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hc : HasCompactSupport g) (hs : tsupport g⊆U) :
        ∃ C : ℝ,0<C ∧ ∀ h : ℝ,0≤h → h≤1 → ∀ z : Fin 3 → ℂ,
          ∀ q : HV,∀ v : Fin 3 → S,
          (∀ i,LocalEqual U (sobolevInjection 1 (q i)) (physicalAug z v i : Dist)) →
          sobNorm h 1 (physicalAug z (fun i => mult g (v i)))≤C*‖q‖ := by
    …

    Mentions: OAI.ElasticityCGO.S

52. theorem OAI.ElasticityCGO.physical_column_localized_realization line 822

    Source documentation

    The actual physical CGO corrections have a uniform localized augmented semiclassical H1 bound. Localize the displacement and then take its actual shifted divergence: the scalar is not a separately prescribed amplitude.

    theorem physical_column_localized_realization (R : ℝ) (hR : 1≤R) (α β : X)
        (lam m : Smooth) (hl : ExteriorConstant lam) (hm : ExteriorConstant m)
        (a : ℕ → Amplitude Smooth) (ha : PhysicalColumn R hR α β lam m a)
        {g : X → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hc : HasCompactSupport g)
        (hs : tsupport g⊆Metric.ball 0 R) :
        ∃ C h₀ : ℝ,0<C ∧ 0<h₀ ∧ h₀≤1 ∧ ∀ h : ℝ,0<h → h≤h₀ →
          ∃ w : ElasticityPhysicalDual.H,∃ q : HV,∃ v : Fin 3 → S,
            (∀ i,∀ᵐ x ∂(volume : Measure X),x∈Metric.ball 0 R → w i x=v i x) ∧
            (∀ i,EqOn (physical 0 lam m (cgoField R hR h α β a v) i : X → ℂ) 0 (Metric.ball 0 R)) ∧
            (∀ i,sobolevInjection 1 (q i)=smulLeftCLM ℂ (fiveCutoff R hR 0)
              ((Fin.cons (divd (phase h α β) (fun j => (w j : Dist)))
                (fun j => (w j : Dist)) : Fin 4 → Dist) i)) ∧
    …

    Mentions: OAI.ElasticityCGO.PhysicalColumn, OAI.ElasticityPhysicalDual.H, OAI.ElasticityCGO.S, OAI.ElasticityCGO.cgoField, OAI.ElasticityCGO.fiveCutoff

53. theorem OAI.ElasticityCGO.physical_column_shifted_realization line 860

    Source documentation

    The actual physical CGO corrections have a uniform localized augmented semiclassical H1 bound. Localize the displacement and then take its actual shifted divergence: the scalar is not a separately prescribed amplitude.

    theorem physical_column_shifted_realization (R : ℝ) (hR : 1≤R) (α β : X)
        (lam m : Smooth)
        (a : ℕ → Amplitude Smooth) (ha : PhysicalColumn R hR α β lam m a)
        {g : X → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hc : HasCompactSupport g)
        (hs : tsupport g⊆Metric.ball 0 R) :
        ∃ C h₀ : ℝ,0<C ∧ 0<h₀ ∧ h₀≤1 ∧ ∀ h : ℝ,0<h → h≤h₀ →
          ∃ w : ElasticityPhysicalDual.H,∃ q : HV,∃ v : Fin 3 → S,
            (∀ i,∀ᵐ x ∂(volume : Measure X),x∈Metric.ball 0 R → w i x=v i x) ∧
            (∀ i,EqOn (physical (phase h α β) lam m
              ((fun j => cut ⟨fiveCutoff R hR 0,fiveCutoff_smooth R hR 0⟩ (fiveCutoff_compact R hR 0)
                ((truncation (h : ℂ) 8 a).1 j))-v) i : X → ℂ) 0 (Metric.ball 0 R)) ∧
            (∀ i,sobolevInjection 1 (q i)=smulLeftCLM ℂ (fiveCutoff R hR 0)
    …

    Mentions: OAI.ElasticityCGO.PhysicalColumn, OAI.ElasticityPhysicalDual.H, OAI.ElasticityCGO.S, OAI.ElasticityCGO.cut, OAI.ElasticityCGO.fiveCutoff, OAI.ElasticityCGO.fiveCutoff_smooth, OAI.ElasticityCGO.fiveCutoff_compact

54. lemma OAI.ElasticityAugmented.restrict_divT line 901
55. theorem OAI.ElasticityAugmented.truncation_divergence_on line 907

    Source documentation

    The actual finite divergence constraint on an open physical region.

    theorem truncation_divergence_on {U : Set X} (hU : IsOpen U)
        (θ : Fin 3 → ℂ) (h : ℂ) (hh : h≠0) (N : ℕ) (a : ℕ → Amplitude Smooth)
        (h₀ : normal θ (a 0).1=0)
        (hrec : ∀ j<N,EqOn (fun x => ((normal θ (a (j+1)).1 : Smooth) : X → ℂ) x)
          (fun x => ((-(div coord (a j).1-(a j).2) : Smooth) : X → ℂ) x) U) :
        EqOn ((divT (shifted coord (h⁻¹ • θ)) (truncation h N a).1 : Smooth) : X → ℂ)
          (((truncation h N a).2+h^N • (div coord (a N).1-(a N).2) : Smooth) : X → ℂ) U := by
    …

    Mentions: OAI.ElasticityAugmented.X, OAI.ElasticityAugmented.Amplitude, OAI.ElasticityAugmented.Smooth, OAI.ElasticityAugmented.normal, OAI.ElasticityAugmented.div, OAI.ElasticityAugmented.coord, OAI.ElasticityAugmented.divT, OAI.ElasticityAugmented.shifted, OAI.ElasticityAugmented.truncation

56. lemma OAI.ElasticityCGO.divShift_cut_local line 933
57. theorem OAI.ElasticityCGO.cut_truncation_divergence line 947

    Source documentation

    The exact scalar augmented amplitude has the same eight-order truncation plus a single h^8 defect. No unjustified differentiation of small L2 errors.

    theorem cut_truncation_divergence {U : Set X} (hU : IsOpen U)
        (θ : Fin 3 → ℂ) (h : ℂ) (hh : h≠0) (N : ℕ) (a : ℕ → Amplitude Smooth)
        (h₀ : normal θ (a 0).1=0)
        (hrec : ∀ j<N,EqOn (fun x => ((normal θ (a (j+1)).1 : Smooth) : X → ℂ) x)
          (fun x => ((-(div coord (a j).1-(a j).2) : Smooth) : X → ℂ) x) U)
        (χ : Smooth) (hc : HasCompactSupport (χ : X → ℂ)) (hχ : EqOn (χ : X → ℂ) 1 U) :
        EqOn (divShift (h⁻¹ • θ) (fun j => cut χ hc ((truncation h N a).1 j)) : X → ℂ)
          (cut χ hc ((truncation h N a).2+h^N • (div coord (a N).1-(a N).2))) U := by
    …

    Mentions: OAI.ElasticityCGO.cut

58. lemma OAI.ElasticityCGO.semiclassical_H1_le_H1 line 971
59. theorem OAI.ElasticityCGO.finite_polynomial_H1_bound line 982

    Source documentation

    A literal finite Schwartz amplitude polynomial is uniformly bounded in the semiclassical H1 norm. There is no h-dependent Sobolev constant.

    theorem finite_polynomial_H1_bound (N : ℕ) (f : ℕ → S) (h : ℝ)
        (hh : 0≤h) (hh1 : h≤1) :
        norm2 (J h 1 (truncation (h : ℂ) N f))≤
          ∑ j ∈ Finset.range (N+1),norm2 (J 1 1 (f j)) := by
    …

    Mentions: OAI.ElasticityCGO.S

60. lemma OAI.ElasticityCGO.cut_truncation line 996
61. theorem OAI.ElasticityCGO.cut_polynomial_H1_bound line 1004

    Source documentation

    The formal smooth amplitudes need no global growth hypothesis: after the actual compact cutoff, their finite order-eight truncations have a uniform H_h^1 bound.

    theorem cut_polynomial_H1_bound (χ : Smooth) (hc : HasCompactSupport (χ : X → ℂ))
        (N : ℕ) (a : ℕ → Smooth) :
        ∃ C : ℝ,0<C ∧ ∀ h : ℝ,0≤h → h≤1 →
          norm2 (J h 1 (cut χ hc (truncation (h : ℂ) N a)))≤C := by
    …

    Mentions: OAI.ElasticityCGO.cut

62. lemma OAI.ElasticityCGO.truncation_scalar line 1022
63. lemma OAI.ElasticityCGO.truncation_vector line 1030
64. lemma OAI.ElasticityCGO.mult_eq_of_local line 1039
65. lemma OAI.ElasticityCGO.H1_monomial_bound line 1048
66. theorem OAI.ElasticityCGO.localized_formal_divergence_H1_bound line 1057

    Source documentation

    The formal divergence, localized strictly inside the physical region, is uniformly H_h^1 bounded. The apparent h⁻¹ term is removed by the actual finite divergence recurrence, not by estimating an independent scalar.

    theorem localized_formal_divergence_H1_bound {U : Set X} (hU : IsOpen U)
        (θ : Fin 3 → ℂ) (N : ℕ) (a : ℕ → Amplitude Smooth)
        (h₀ : normal θ (a 0).1=0)
        (hrec : ∀ j<N,EqOn (fun x => ((normal θ (a (j+1)).1 : Smooth) : X → ℂ) x)
          (fun x => ((-(div coord (a j).1-(a j).2) : Smooth) : X → ℂ) x) U)
        (χ : Smooth) (hc : HasCompactSupport (χ : X → ℂ)) (hχ : EqOn (χ : X → ℂ) 1 U)
        {g : X → ℂ} (hg : g.HasTemperateGrowth) (hs : tsupport g⊆U) :
        ∃ C : ℝ,0<C ∧ ∀ h : ℝ,0<h → h≤1 →
          norm2 (J h 1 (mult g (divShift ((h : ℂ)⁻¹ • θ)
            (fun j => cut χ hc ((truncation (h : ℂ) N a).1 j)))))≤C := by
    …

    Mentions: OAI.ElasticityCGO.cut

67. lemma OAI.ElasticityCGO.mult_cut_truncation_vector line 1100
68. theorem OAI.ElasticityCGO.localized_formal_augmented_H1_bound line 1111

    Source documentation

    Fixed interior localization of the whole formal physical displacement has a uniformly bounded ACTUAL four-component H_h^1 amplitude. The singular phase is cancelled by the actual divergence recurrence.

    theorem localized_formal_augmented_H1_bound {U : Set X} (hU : IsOpen U)
        (θ : Fin 3 → ℂ) (N : ℕ) (a : ℕ → Amplitude Smooth)
        (h₀ : normal θ (a 0).1=0)
        (hrec : ∀ j<N,EqOn (fun x => ((normal θ (a (j+1)).1 : Smooth) : X → ℂ) x)
          (fun x => ((-(div coord (a j).1-(a j).2) : Smooth) : X → ℂ) x) U)
        (χ : Smooth) (hc : HasCompactSupport (χ : X → ℂ)) (hχ : EqOn (χ : X → ℂ) 1 U)
        {g : X → ℂ} (hg : g.HasTemperateGrowth) (hs : tsupport g⊆U) :
        ∃ C : ℝ,0<C ∧ ∀ h : ℝ,0<h → h≤1 →
          sobNorm h 1 (physicalAug ((h : ℂ)⁻¹ • θ)
            (fun i => mult g (cut χ hc ((truncation (h : ℂ) N a).1 i))))≤C := by
    …

    Mentions: OAI.ElasticityCGO.cut

69. lemma OAI.ElasticityCGO.sobNorm_sub_four line 1162
70. theorem OAI.ElasticityCGO.localized_actual_amplitude_bound line 1175

    Source documentation

    Literal original-PDE CGO solutions can be chosen with a uniformly bounded actual compact augmented amplitude. Both the formal divergence and the correction divergence are proved bounds, not additional assumptions.

    theorem localized_actual_amplitude_bound (R : ℝ) (hR : 1≤R) (α β : X)
        (lam m : Smooth) (hl : ExteriorConstant lam) (hm : ExteriorConstant m)
        (a : ℕ → Amplitude Smooth) (ha : PhysicalColumn R hR α β lam m a)
        (h₀ : normal (fun i => (α i : ℂ)+Complex.I*(β i : ℂ)) (a 0).1=0)
        (hrec : ∀ j<8,EqOn
          (fun x => ((normal (fun i => (α i : ℂ)+Complex.I*(β i : ℂ)) (a (j+1)).1 : Smooth) : X → ℂ) x)
          (fun x => ((-(div coord (a j).1-(a j).2) : Smooth) : X → ℂ) x) (Metric.ball 0 R))
        {g : X → ℂ} (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hc : HasCompactSupport g)
        (hs : tsupport g⊆Metric.ball 0 R) :
        ∃ C h₁ : ℝ,0<C ∧ 0<h₁ ∧ ∀ h : ℝ,0<h → h≤h₁ → ∃ v : Fin 3 → S,
          (∀ i,EqOn (physical 0 lam m (cgoField R hR h α β a v) i : X → ℂ) 0 (Metric.ball 0 R)) ∧
          sobNorm h 1 (physicalAug (phase h α β) (fun i => mult g
    …

    Mentions: OAI.ElasticityCGO.PhysicalColumn, OAI.ElasticityCGO.S, OAI.ElasticityCGO.cgoField