OAI/MathematicalPhysics/Elasticity/CGO.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElasticityAugmented.leadingR_add line 13
2. lemma OAI.ElasticityAugmented.leadingS_add line 16
3. lemma OAI.ElasticityAugmented.normal_add line 20
4. def OAI.ElasticityAugmented.localAmp line 24
5. def OAI.ElasticityAugmented.CompatibleOn line 26
6. def OAI.ElasticityAugmented.RecursOn line 32
7. lemma OAI.ElasticityAugmented.recurs_compatible line 40
8. theorem OAI.ElasticityAugmented.exists_physical_recursion_step line 52

   Source documentation

   One actual smooth recursive step, solving all three physical equations. The open-region restriction algebra certifies differentiated compatibility; continuity extends the tangent source to its compact closure for transport.

   theorem exists_physical_recursion_step {U : Set X} (hU : IsOpen U) (hC : IsCompact (closure U))
       (θ : Fin 3 → ℂ) (hθ : ∑ i,θ i*θ i=0) (hne : θ≠0)
       (k r : Smooth) (hr : ∀ x,(r : X → ℂ) x≠0) (hk : ∀ x,(k : X → ℂ) x≠0)
       (hl : ∀ x,((k+r*r : Smooth) : X → ℂ) x≠0)
       (a : Amplitude Smooth) (ha : CompatibleOn hU θ (k-r*r) (r*r) a) :
       ∃ b : Amplitude Smooth, RecursOn hU θ (k-r*r) (r*r) a b ∧
         CompatibleOn hU θ (k-r*r) (r*r) b := by
   …

   Mentions: OAI.ElasticityAugmented.X, OAI.ElasticityAugmented.Smooth, OAI.ElasticityAugmented.Amplitude, OAI.ElasticityAugmented.CompatibleOn, OAI.ElasticityAugmented.RecursOn

9. theorem OAI.ElasticityAugmented.exists_recursive_series line 128

   Source documentation

   Every compatible smooth amplitude has an actual infinite recursive sequence; only its finite truncations are used. There is no formal-solvability hypothesis.

   theorem exists_recursive_series {U : Set X} (hU : IsOpen U) (hC : IsCompact (closure U))
       (θ : Fin 3 → ℂ) (hθ : ∑ i,θ i*θ i=0) (hne : θ≠0)
       (k r : Smooth) (hr : ∀ x,(r : X → ℂ) x≠0) (hk : ∀ x,(k : X → ℂ) x≠0)
       (hl : ∀ x,((k+r*r : Smooth) : X → ℂ) x≠0)
       (a₀ : Amplitude Smooth) (ha₀ : CompatibleOn hU θ (k-r*r) (r*r) a₀) :
       ∃ a : ℕ → Amplitude Smooth, a 0=a₀ ∧
         (∀ j,RecursOn hU θ (k-r*r) (r*r) (a j) (a (j+1))) ∧
         ∀ j,CompatibleOn hU θ (k-r*r) (r*r) (a j) := by
   …

   Mentions: OAI.ElasticityAugmented.X, OAI.ElasticityAugmented.Smooth, OAI.ElasticityAugmented.Amplitude, OAI.ElasticityAugmented.CompatibleOn, OAI.ElasticityAugmented.RecursOn

10. theorem OAI.ElasticityAugmented.exists_physical_formal_frame line 148

    Source documentation

    The given genuine leading frame develops to physical compatible amplitudes, with all three recursive equations on the same open region.

    theorem exists_physical_formal_frame {U : Set X} (hU : IsOpen U) (hC : IsCompact (closure U))
        (θ : Fin 3 → ℂ) (hθ : ∑ i,θ i*θ i=0) (hne : θ≠0)
        (k r : Smooth) (hr : ∀ x,(r : X → ℂ) x≠0) (hk : ∀ x,(k : X → ℂ) x≠0)
        (hl : ∀ x,((k+r*r : Smooth) : X → ℂ) x≠0) :
        ∃ a : Fin 3 → ℕ → Amplitude Smooth,
        ∃ B : X → Module.Basis (Fin 3) ℂ (ElasticityFrame.Fiber θ),
          (∀ ν,normal θ (a ν 0).1=0) ∧
          (∀ ν,leadingR (localCoord hU) θ (restrictSmooth U (k-r*r)) (restrictSmooth U (r*r))
              (localAmp U (a ν 0)).1 (localAmp U (a ν 0)).2=0 ∧
            leadingS (localCoord hU) θ (restrictSmooth U (k-r*r)) (restrictSmooth U (r*r))
              (localAmp U (a ν 0)).1 (localAmp U (a ν 0)).2=0) ∧
          (∀ ν j,RecursOn hU θ (k-r*r) (r*r) (a ν j) (a ν (j+1))) ∧
    …

    Mentions: OAI.ElasticityAugmented.X, OAI.ElasticityAugmented.Smooth, OAI.ElasticityAugmented.Amplitude, OAI.ElasticityFrame.Fiber, OAI.ElasticityAugmented.normal, OAI.ElasticityAugmented.leadingR, OAI.ElasticityAugmented.localCoord, OAI.ElasticityAugmented.restrictSmooth, OAI.ElasticityAugmented.localAmp, OAI.ElasticityAugmented.leadingS, OAI.ElasticityAugmented.RecursOn

11. def OAI.ElasticityAugmented.localAmpLM line 198
12. lemma OAI.ElasticityAugmented.localAmp_truncation line 202
13. lemma OAI.ElasticityAugmented.restrict_shifted line 205
14. lemma OAI.ElasticityAugmented.restrict_LT line 208
15. theorem OAI.ElasticityAugmented.physical_truncation_residual_on line 217

    Source documentation

    Literal finite physical residual on an open region. All compatibility identities are local equalities, not strengthened global transport hypotheses.

    theorem physical_truncation_residual_on {U : Set X} (hU : IsOpen U)
        (θ : Fin 3 → ℂ) (hθ : ∑ i,θ i*θ i=0) (lam m : Smooth)
        (h : ℂ) (hh : h≠0) (N : ℕ) (a : ℕ → Amplitude Smooth)
        (hR₀ : leadingR (localCoord hU) θ (restrictSmooth U lam) (restrictSmooth U m)
          (localAmp U (a 0)).1 (localAmp U (a 0)).2=0)
        (hn₀ : normal θ (a 0).1=0)
        (hrec : ∀ j<N,RecursOn hU θ lam m (a j) (a (j+1))) (i : Fin 3) :
        EqOn ((LT (shifted coord (h⁻¹ • θ)) lam m (truncation h N a).1 i : Smooth) : X → ℂ)
          ((h^N • (R coord lam m (a N).1 (a N).2 i+
            (lam+m)*coord i (div coord (a N).1-(a N).2)+
            coord i lam*(div coord (a N).1-(a N).2)+
            (h⁻¹*θ i) • ((lam+m)*(div coord (a N).1-(a N).2))) : Smooth) : X → ℂ) U := by
    …

    Mentions: OAI.ElasticityAugmented.X, OAI.ElasticityAugmented.Smooth, OAI.ElasticityAugmented.Amplitude, OAI.ElasticityAugmented.leadingR, OAI.ElasticityAugmented.localCoord, OAI.ElasticityAugmented.restrictSmooth, OAI.ElasticityAugmented.localAmp, OAI.ElasticityAugmented.normal, OAI.ElasticityAugmented.RecursOn, OAI.ElasticityAugmented.LT, OAI.ElasticityAugmented.shifted, OAI.ElasticityAugmented.coord, OAI.ElasticityAugmented.truncation, OAI.ElasticityAugmented.R, OAI.ElasticityAugmented.div

16. lemma OAI.ElasticityRegularity.exists_bounded_integer_multiplier line 252
17. lemma OAI.ElasticityRegularity.nested_multiplier line 263
18. lemma OAI.ElasticityRegularity.laplacian_product_divergence line 276
19. theorem OAI.ElasticityRegularity.quantitative_cutoff_gain line 295

    Source documentation

    A nested-cutoff interior norm estimate for the genuine distributional Laplacian. All multiplier and derivative constants are produced by previously proved closed graph arguments. The result includes the initial negative order.

    theorem quantitative_cutoff_gain (k : ℤ) {χ η : E → ℂ}
        (hχ : ContDiff ℝ (⊤ : ℕ∞) χ) (hcχ : HasCompactSupport χ)
        (hη : ContDiff ℝ (⊤ : ℕ∞) η) (hcη : HasCompactSupport η)
        (h1 : Set.EqOn η 1 (tsupport χ)) :
        ∃ C : ℝ, 0<C ∧ ∀ (u : 𝓢'(E,ℂ)) (f g : Lp ℂ 2 (volume : Measure E)),
          sobolevInjection (k : ℝ) f=smulLeftCLM ℂ η u →
          sobolevInjection ((k : ℝ)-1) g=smulLeftCLM ℂ η (Δ u) →
          ∃ q : Lp ℂ 2 (volume : Measure E),
            sobolevInjection ((k : ℝ)+1) q=smulLeftCLM ℂ χ u ∧
            ‖q‖ ≤ C*(‖f‖+‖g‖) := by
    …

    Mentions: OAI.ElasticityRegularity.sobolevInjection

20. theorem OAI.ElasticityRegularity.exists_localized_derivative line 370

    Source documentation

    A genuine localized first derivative has a bounded realization from the larger cutoff's Sobolev data. This also holds at negative integers.

    theorem exists_localized_derivative (k : ℤ) {a η : E → ℂ}
        (ha : ContDiff ℝ (⊤ : ℕ∞) a) (hca : HasCompactSupport a)
        (hη : ContDiff ℝ (⊤ : ℕ∞) η) (hcη : HasCompactSupport η)
        (h1 : Set.EqOn η 1 (tsupport a)) (v : E) :
        ∃ L : Lp ℂ 2 (volume : Measure E) →L[ℂ] Lp ℂ 2 (volume : Measure E),
          ∀ u f, sobolevInjection (k : ℝ) f=smulLeftCLM ℂ η u →
            sobolevInjection ((k : ℝ)-1) (L f)=smulLeftCLM ℂ a (∂_{v} u) := by
    …

    Mentions: OAI.ElasticityRegularity.sobolevInjection

21. theorem OAI.ElasticityRegularity.exists_localized_multiplier line 392

    Source documentation

    A bounded zeroth-order realization with one order of harmless loss.

    theorem exists_localized_multiplier (k : ℤ) {a η : E → ℂ}
        (ha : ContDiff ℝ (⊤ : ℕ∞) a) (hca : HasCompactSupport a)
        (hη : ContDiff ℝ (⊤ : ℕ∞) η) (hcη : HasCompactSupport η)
        (h1 : Set.EqOn η 1 (tsupport a)) :
        ∃ L : Lp ℂ 2 (volume : Measure E) →L[ℂ] Lp ℂ 2 (volume : Measure E),
          ∀ u f, sobolevInjection (k : ℝ) f=smulLeftCLM ℂ η u →
            sobolevInjection ((k : ℝ)-1) (L f)=smulLeftCLM ℂ a u := by
    …

    Mentions: OAI.ElasticityRegularity.sobolevInjection

22. theorem OAI.ElasticityRegularity.quadratic_parameter_norm line 410

    Source documentation

    The precise polynomial loss for the shifted scalar-principal system.

    theorem quadratic_parameter_norm {W ι : Type*} [NormedAddCommGroup W]
        [NormedSpace ℂ W] [Fintype ι] (R₀ R₂ : W) (R₁ : ι → W) :
        ∃ C : ℝ, 0<C ∧ ∀ z : ι → ℂ,
          ‖R₀+(∑ i, z i • R₁ i)+(∑ i, z i*z i) • R₂‖ ≤ C*(1+∑ i, ‖z i‖)^2 := by
    …

23. abbrev OAI.ElasticityDistribution.H line 462
24. abbrev OAI.ElasticityDistribution.HV line 463
25. def OAI.ElasticityDistribution.lowerPart line 465
26. lemma OAI.ElasticityDistribution.cutoff_coeff line 470
27. lemma OAI.ElasticityDistribution.coeff_complex_smul line 474
28. theorem OAI.ElasticityDistribution.exists_lower_realization line 479

    Source documentation

    The actual lower-order shifted augmented operator, localized on a smaller cutoff, is polynomial in the phase with bounded Sobolev coefficients.

    theorem exists_lower_realization (k : ℤ) {η ξ : X → ℂ}
        (hη : ContDiff ℝ (⊤ : ℕ∞) η) (hcη : HasCompactSupport η)
        (hξ : ContDiff ℝ (⊤ : ℕ∞) ξ) (hcξ : HasCompactSupport ξ)
        (h1 : Set.EqOn ξ 1 (tsupport η))
        (A : Fin 3 → Fin 4 → Fin 4 → Coeff) (V : Fin 4 → Fin 4 → Coeff) (i : Fin 4) :
        ∃ L₀ L₂ : HV →L[ℂ] H, ∃ L₁ : Fin 3 → HV →L[ℂ] H,
          ∀ (z : Fin 3 → ℂ) (U : Fin 4 → Dist) (f : HV),
            (∀ j, sobolevInjection (k : ℝ) (f j)=smulLeftCLM ℂ ξ (U j)) →
            sobolevInjection ((k : ℝ)-1)
              ((L₀+(∑ d, z d • L₁ d)+(∑ d, z d*z d) • L₂) f)=
                smulLeftCLM ℂ η (lowerPart z A V U i) := by
    …

    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.HV, OAI.ElasticityDistribution.H, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.lowerPart

29. theorem OAI.ElasticityDistribution.lower_realization_bound line 523

    Source documentation

    A fixed quadratic phase loss, with no elliptic estimate assumed.

    theorem lower_realization_bound (k : ℤ) {η ξ : X → ℂ}
        (hη : ContDiff ℝ (⊤ : ℕ∞) η) (hcη : HasCompactSupport η)
        (hξ : ContDiff ℝ (⊤ : ℕ∞) ξ) (hcξ : HasCompactSupport ξ)
        (h1 : Set.EqOn ξ 1 (tsupport η))
        (A : Fin 3 → Fin 4 → Fin 4 → Coeff) (V : Fin 4 → Fin 4 → Coeff) (i : Fin 4) :
        ∃ C : ℝ, 0<C ∧ ∀ (z : Fin 3 → ℂ) (U : Fin 4 → Dist) (f : HV),
          (∀ j, sobolevInjection (k : ℝ) (f j)=smulLeftCLM ℂ ξ (U j)) →
          ∃ q : H, sobolevInjection ((k : ℝ)-1) q=smulLeftCLM ℂ η (lowerPart z A V U i) ∧
            ‖q‖ ≤ C*(1+∑ d, ‖z d‖)^2*‖f‖ := by
    …

    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.HV, OAI.ElasticityDistribution.H, OAI.ElasticityDistribution.lowerPart

30. lemma OAI.ElasticityDistribution.normalized_laplacian line 538
31. theorem OAI.ElasticityDistribution.scalar_principal_quantitative_gain line 548

    Source documentation

    One genuine interior regularity gain, with a phase-uniform polynomial bound. There are no unproved local regularity assumptions: the input is actual Sobolev representatives at the previous, possibly negative, integer order.

    theorem scalar_principal_quantitative_gain (k : ℤ) {Ω : Set X} {χ η ξ : X → ℂ}
        (hχ : ContDiff ℝ (⊤ : ℕ∞) χ) (hcχ : HasCompactSupport χ)
        (hη : ContDiff ℝ (⊤ : ℕ∞) η) (hcη : HasCompactSupport η)
        (hξ : ContDiff ℝ (⊤ : ℕ∞) ξ) (hcξ : HasCompactSupport ξ)
        (h1 : Set.EqOn η 1 (tsupport χ)) (h2 : Set.EqOn ξ 1 (tsupport η))
        (hsη : tsupport η ⊆ Ω)
        (A : Fin 3 → Fin 4 → Fin 4 → Coeff) (V : Fin 4 → Fin 4 → Coeff) :
        ∃ C : ℝ, 0<C ∧ ∀ (z : Fin 3 → ℂ) (U F : Fin 4 → Dist) (f g : HV),
          (∀ i, LocalEq Ω (Δ (U i)+lowerPart z A V U i) (F i)) →
          (∀ i, sobolevInjection (k : ℝ) (f i)=smulLeftCLM ℂ ξ (U i)) →
          (∀ i, sobolevInjection ((k : ℝ)-1) (g i)=smulLeftCLM ℂ η (F i)) →
          ∃ q : HV, (∀ i, sobolevInjection ((k : ℝ)+1) (q i)=smulLeftCLM ℂ χ (U i)) ∧
    …

    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.HV, OAI.ElasticityDistribution.LocalEq, OAI.ElasticityDistribution.lowerPart

32. theorem OAI.ElasticityDistribution.normalized_quantitative_gain line 612

    Source documentation

    The preceding estimate applies to the actual normalized physical system.

    theorem normalized_quantitative_gain (k : ℤ) {Ω : Set X} {χ η ξ : X → ℂ}
        (hχ : ContDiff ℝ (⊤ : ℕ∞) χ) (hcχ : HasCompactSupport χ)
        (hη : ContDiff ℝ (⊤ : ℕ∞) η) (hcη : HasCompactSupport η)
        (hξ : ContDiff ℝ (⊤ : ℕ∞) ξ) (hcξ : HasCompactSupport ξ)
        (h1 : Set.EqOn η 1 (tsupport χ)) (h2 : Set.EqOn ξ 1 (tsupport η))
        (hsη : tsupport η ⊆ Ω) (lam m n o : Coeff) (hn : n*m=1) (ho : o*(lam+m+m)=1) :
        ∃ C : ℝ, 0<C ∧ ∀ (z : Fin 3 → ℂ) (U F : Fin 4 → Dist) (f g : HV),
          (∀ i, LocalEq Ω (normPair z lam m n o (fun j => U j.succ) (U 0) i) (F i)) →
          (∀ i, sobolevInjection (k : ℝ) (f i)=smulLeftCLM ℂ ξ (U i)) →
          (∀ i, sobolevInjection ((k : ℝ)-1) (g i)=smulLeftCLM ℂ η (F i)) →
          ∃ q : HV, (∀ i, sobolevInjection ((k : ℝ)+1) (q i)=smulLeftCLM ℂ χ (U i)) ∧
            ‖q‖ ≤ C*(1+∑ d, ‖z d‖)^2*(‖f‖+‖g‖) := by
    …

    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.HV, OAI.ElasticityDistribution.LocalEq, OAI.ElasticityDistribution.normPair

33. abbrev OAI.ElasticityDistribution.H3 line 631
34. lemma OAI.ElasticityDistribution.complex_zero_dist line 632
35. lemma OAI.ElasticityDistribution.complex_smul_dist_zero line 633
36. def OAI.ElasticityDistribution.lpProj line 635
37. def OAI.ElasticityDistribution.divZeroCLM line 637
38. lemma OAI.ElasticityDistribution.divZeroCLM_apply line 639
39. lemma OAI.ElasticityDistribution.divd_affine line 643
40. theorem OAI.ElasticityDistribution.affine_cutoff_bound line 649

    Source documentation

    A bounded Sobolev realization of an actual affine distribution family. All mapping properties are proved in the concrete applications below.

    theorem affine_cutoff_bound (s : ℝ) {η : X → ℂ}
        (T₀ : H3 →L[ℂ] Dist) (T₁ : Fin 3 → H3 →L[ℂ] Dist)
        (h₀ : ∀ f, MemSobolev s 2 (smulLeftCLM ℂ η (T₀ f)))
        (h₁ : ∀ d f, MemSobolev s 2 (smulLeftCLM ℂ η (T₁ d f))) :
        ∃ C : ℝ, 0<C ∧ ∀ (z : Fin 3 → ℂ) (f : H3),
          ∃ q : ElasticityDistribution.H,
            sobolevInjection s q=smulLeftCLM ℂ η (T₀ f+∑ d, z d • T₁ d f) ∧
            ‖q‖ ≤ C*(1+∑ d, ‖z d‖)^2*‖f‖ := by
    …

    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.H3, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.H

41. theorem OAI.ElasticityDistribution.augmentation_cutoff_bound line 673

    Source documentation

    Localized actual physical augmentation starts in H^-1 with polynomial phase loss; its scalar component is the shifted divergence, not a new unknown.

    theorem augmentation_cutoff_bound {η : X → ℂ}
        (hη : ContDiff ℝ (⊤ : ℕ∞) η) (hcη : HasCompactSupport η) :
        ∃ C : ℝ, 0<C ∧ ∀ (z : Fin 3 → ℂ) (f : H3),
          ∃ q : HV, (∀ i, sobolevInjection (-1) (q i)=smulLeftCLM ℂ η
            ((Fin.cons (divd z (fun j => (f j : Dist))) (fun j => (f j : Dist)) : Fin 4 → Dist) i)) ∧
            ‖q‖ ≤ C*(1+∑ d, ‖z d‖)^2*‖f‖ := by
    …

    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.H3, OAI.ElasticityDistribution.HV, OAI.ElasticityDistribution.divd, OAI.ElasticityDistribution.Dist

42. theorem OAI.ElasticityDistribution.normSource_cutoff_bound line 717

    Source documentation

    The source of the actual normalized system is also H^-1, with a uniform polynomial phase bound depending on the fixed coefficients and cutoff only.

    theorem normSource_cutoff_bound {η : X → ℂ}
        (hη : ContDiff ℝ (⊤ : ℕ∞) η) (hcη : HasCompactSupport η) (m n o : Coeff) :
        ∃ C : ℝ, 0<C ∧ ∀ (z : Fin 3 → ℂ) (f : H3),
          ∃ q : HV, (∀ i, sobolevInjection (-1) (q i)=smulLeftCLM ℂ η
            (normSource z m n o (fun j => (f j : Dist)) i)) ∧
            ‖q‖ ≤ C*(1+∑ d, ‖z d‖)^2*‖f‖ := by
    …

    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.H3, OAI.ElasticityDistribution.HV, OAI.ElasticityDistribution.normSource, OAI.ElasticityDistribution.Dist

43. lemma OAI.ElasticityDistribution.norm_pi_map_le line 775
44. theorem OAI.ElasticityDistribution.physical_quantitative_H1 line 784

    Source documentation

    Two interior gains for a genuine physical L2 solution, starting with its actual H^-1 divergence, suffice for a polynomially bounded H^1 augmented remainder. Arbitrarily high finite CGO expansions absorb this fixed loss.

    theorem physical_quantitative_H1 {Ω : Set X} (χ : Fin 5 → X → ℂ)
        (hχ : ∀ i, ContDiff ℝ (⊤ : ℕ∞) (χ i)) (hcχ : ∀ i, HasCompactSupport (χ i))
        (hnest : ∀ i : Fin 4, Set.EqOn (χ i.succ) 1 (tsupport (χ i.castSucc)))
        (hs : ∀ i, tsupport (χ i) ⊆ Ω)
        (lam m n o : Coeff) (hn : n*m=1) (ho : o*(lam+m+m)=1) :
        ∃ C : ℝ, 0<C ∧ ∀ (z : Fin 3 → ℂ) (r F : H3),
          (∀ i, LocalEq Ω (phys z lam m (fun j => (r j : Dist)) i) (F i : Dist)) →
          ∃ q : HV, (∀ i, sobolevInjection 1 (q i)=smulLeftCLM ℂ (χ 0)
            ((Fin.cons (divd z (fun j => (r j : Dist))) (fun j => (r j : Dist)) : Fin 4 → Dist) i)) ∧
            ‖q‖ ≤ C*(1+∑ d, ‖z d‖)^6*(‖r‖+‖F‖) := by
    …

    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.H3, OAI.ElasticityDistribution.LocalEq, OAI.ElasticityDistribution.phys, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.HV, OAI.ElasticityDistribution.divd

45. lemma OAI.ElasticityDistribution.norm_ofLp_le line 862
46. lemma OAI.ElasticityDistribution.phase_envelope line 865
47. theorem OAI.ElasticityDistribution.physical_quantitative_correction line 877

    Source documentation

    Actual physical correction with a proved polynomial interior bound. This uses the uniform physical inverse and two true interior elliptic gains; taking more terms in the finite CGO expansion absorbs its fixed sixth-power loss.

    theorem physical_quantitative_correction (R : ℝ) (hR : 1≤R)
        (Ω : Set X) (hΩ : Ω ⊆ Metric.closedBall 0 R) (α β : X) (hα : α ≠ 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, Set.EqOn (χ i.succ) 1 (tsupport (χ i.castSucc)))
        (hs : ∀ i, tsupport (χ i) ⊆ Ω) :
        ∃ C h₀ : ℝ, 0<C ∧ 0<h₀ ∧ ∀ h : ℝ, 0<h → h≤h₀ →
    …

    Mentions: OAI.ElasticityDistribution.X

48. theorem OAI.ElasticityDistribution.classical_quantitative_correction line 936

    Source documentation

    The quantitative correction and classical representative are the SAME physical solution. In particular no smooth solvability estimate is postulated.

    theorem classical_quantitative_correction (R : ℝ) (hR : 1≤R)
        (Ω Ω' : Set X) (hΩ : Ω ⊆ Metric.closedBall 0 R) (hΩ' : IsOpen Ω') (hsub : Ω' ⊆ Ω)
        (α β : X) (hα : α ≠ 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, Set.EqOn (χ i.succ) 1 (tsupport (χ i.castSucc)))
        (hs : ∀ i, tsupport (χ i) ⊆ Ω) (h1 : Set.EqOn (χ 0) 1 Ω') :
    …

    Mentions: OAI.ElasticityDistribution.X

49. def OAI.ElasticityDistribution.finiteResidual line 980

    Source documentation

    The two true terms in the physical residual at truncation order eight.

    def finiteResidual (h : ℝ) (f₀ f₁ : Fin 3 → S) : Fin 3 → S :=
    …

    Mentions: OAI.ElasticityDistribution.S

50. lemma OAI.ElasticityDistribution.finiteResidual_bound line 983
51. theorem OAI.ElasticityDistribution.finite_classical_correction line 996

    Source documentation

    Finite physical CGO residuals have a classical correction whose full physical-divergence H1 error tends to zero at an explicit linear rate.

    theorem finite_classical_correction (R : ℝ) (hR : 1≤R)
        (Ω Ω' : Set X) (hΩ : Ω ⊆ Metric.closedBall 0 R) (hΩ' : IsOpen Ω') (hsub : Ω' ⊆ Ω)
        (α β : X) (hα : α ≠ 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, Set.EqOn (χ i.succ) 1 (tsupport (χ i.castSucc)))
        (hs : ∀ i, tsupport (χ i) ⊆ Ω) (h1 : Set.EqOn (χ 0) 1 Ω')
    …

    Mentions: OAI.ElasticityDistribution.X

52. lemma OAI.ElasticityDistribution.correction_cancels_residual line 1038