OAI/MathematicalPhysics/Elasticity/WeakLimits.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

Measure-theoretic core of transverse slicing: a single exceptional null set for all planar tests, obtained using the separable L2 value/derivative graph, not an invalid interchange of an uncountable intersection with almost-everywhere.

  1. lemma OAI.ElasticityDistribution.complex_inr_smul line 13
  2. def OAI.ElasticityDistribution.directiond line 16
  3. def OAI.ElasticityDistribution.normald line 17
  4. def OAI.ElasticityDistribution.leadingRd line 18
  5. def OAI.ElasticityDistribution.leadingSd line 21
  6. lemma OAI.ElasticityDistribution.direction_inr line 26
  7. lemma OAI.ElasticityDistribution.direction_inl line 29
  8. lemma OAI.ElasticityDistribution.leadingR_inr line 32
  9. lemma OAI.ElasticityDistribution.leadingS_inr line 37
  10. theorem OAI.ElasticityDistribution.rd_null_expansion line 45

    Source documentation

    Exact null-phase polynomial decomposition for the physical distributions.

    theorem rd_null_expansion (θ : Fin 3 → ℂ) (hθ : ∑ i, θ i*θ i=0)
    (τ : ℂ) (lam m : Coeff) (u : Fin 3 → Dist) (b : Dist) (i : Fin 3) :
    rd (τ • θ) lam m u b i=rd 0 lam m u b i+τ • leadingRd θ lam m u b i := by
…

    Mentions: OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.rd, OAI.ElasticityDistribution.leadingRd

  11. theorem OAI.ElasticityDistribution.scd_null_expansion line 61
  12. lemma OAI.ElasticityDistribution.divergence_phase line 77
  13. abbrev OAI.ElasticityDistribution.AugHilbert line 88
  14. def OAI.ElasticityDistribution.augEntry line 89
  15. lemma OAI.ElasticityDistribution.augEntry_apply line 93
  16. def OAI.ElasticityDistribution.coeffCLM line 95
  17. def OAI.ElasticityDistribution.ddCLM line 96
  18. def OAI.ElasticityDistribution.sdCLM line 97
  19. def OAI.ElasticityDistribution.lapdCLM line 99
  20. def OAI.ElasticityDistribution.directionCLM line 100
  21. lemma OAI.ElasticityDistribution.coeffCLM_apply line 101
  22. lemma OAI.ElasticityDistribution.ddCLM_apply line 102
  23. lemma OAI.ElasticityDistribution.sdCLM_apply line 103
  24. lemma OAI.ElasticityDistribution.lapdCLM_apply line 104
  25. lemma OAI.ElasticityDistribution.directionCLM_apply line 106
  26. def OAI.ElasticityDistribution.rdCLM line 109
  27. def OAI.ElasticityDistribution.scdCLM line 114
  28. def OAI.ElasticityDistribution.leadingRCLM line 120
  29. def OAI.ElasticityDistribution.leadingSCLM line 124
  30. def OAI.ElasticityDistribution.normalCLM line 129
  31. def OAI.ElasticityDistribution.divergenceCLM line 130
  32. lemma OAI.ElasticityDistribution.rdCLM_apply line 131
  33. lemma OAI.ElasticityDistribution.scdCLM_apply line 135
  34. lemma OAI.ElasticityDistribution.leadingRCLM_apply line 139
  35. lemma OAI.ElasticityDistribution.leadingSCLM_apply line 143
  36. lemma OAI.ElasticityDistribution.normalCLM_apply line 147
  37. lemma OAI.ElasticityDistribution.divergenceCLM_apply line 150
  38. def OAI.ElasticityCGO.augEmbed line 166
  39. lemma OAI.ElasticityCGO.augEmbed_apply line 170
  40. lemma OAI.ElasticityCGO.norm_augEmbed line 171
  41. lemma OAI.ElasticityCGO.norm_augEmbed_le line 174
  42. lemma OAI.ElasticityCGO.norm2_le_sobNorm line 179
  43. lemma OAI.ElasticityCGO.truncation_at_zero line 185
  44. lemma OAI.ElasticityCGO.truncation_continuous line 189
  45. lemma OAI.ElasticityCGO.truncation_tendsto line 192
  46. lemma OAI.ElasticityCGO.formal_scalar_polynomial line 198

    Source documentation

    Exact polynomial formula for the actual localized formal scalar amplitude. The derivative of the localization is retained; it disappears only where g=1.

    lemma formal_scalar_polynomial {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)
    (h : ℂ) (hh : h≠0) :
    divShift (h⁻¹ • θ) (fun i => mult g (cut χ hc ((truncation h N a).1 i)))=
      truncation h N (fun j => mult g (cut χ hc (a j).2))+
      h^N • mult g (cut χ hc (div coord (a N).1-(a N).2))+
      ∑ i, truncation h N (fun j => mult (fun x => fderiv ℝ g x (e i)) (cut χ hc ((a j).1 i))) := by
…

    Mentions: OAI.ElasticityCGO.cut

  47. theorem OAI.ElasticityCGO.formal_augmented_tendsto line 220

    Source documentation

    Strong Schwartz convergence of the formal augmented amplitudes, including its physical scalar component and the cutoff derivative.

    theorem formal_augmented_tendsto {U : Set X} (hU : IsOpen U)
    (θ : Fin 3 → ℂ) (N : ℕ) (hN : 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)
    {g : X → ℂ} (hg : g.HasTemperateGrowth) (hs : tsupport g⊆U)
    {h : ℕ → ℂ} (hh : Tendsto h atTop (𝓝 0)) (hne : ∀ n,h n≠0) :
    ∀ i : Fin 4, Tendsto (fun n => physicalAug ((h n)⁻¹ • θ)
      (fun j => mult g (cut χ hc ((truncation (h n) N a).1 j))) i) atTop
      (𝓝 ((Fin.cons (mult g (cut χ hc (a 0).2)+
        ∑ j, mult (fun x => fderiv ℝ g x (e j)) (cut χ hc ((a 0).1 j)))
…

    Mentions: OAI.ElasticityCGO.cut

  48. lemma OAI.ElasticityCGO.augmented_correction_tendsto line 257

    Source documentation

    A localized actual physical correction with O(h) augmented H_h^1 norm has every literal augmented L2 component converging strongly to zero.

    lemma augmented_correction_tendsto {h : ℕ → ℝ} (hh : Tendsto h atTop (𝓝 0))
    (C : ℝ) (u : ℕ → Fin 4 → S) (hu : ∀ n,sobNorm (h n) 1 (u n)≤C*h n) (i : Fin 4) :
    Tendsto (fun n => L2 (u n i)) atTop (𝓝 0) := by
…

    Mentions: OAI.ElasticityCGO.S

  49. def OAI.ElasticityCGO.localizedFormal line 274
  50. def OAI.ElasticityCGO.localizedLeading line 279
  51. theorem OAI.ElasticityCGO.localized_actual_strong_bound line 289

    Source documentation

    Actual shifted physical solutions, bounded in the literal augmented H1 norm, whose augmented L2 error from the formal series is O(h).

    theorem localized_actual_strong_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) {B : Set X} (hB : IsOpen B)
    (hBR : B⊆Metric.ball 0 R) (hg1 : EqOn g 1 B) :
    ∃ C D h₁ : ℝ,0<C ∧ 0<D ∧ 0<h₁ ∧ ∀ h : ℝ,0<h → h≤h₁ → ∃ u : Fin 3 → S,
      (∀ i,EqOn (physical (phase h α β) lam m u i : X → ℂ) 0 B) ∧
…

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

  52. lemma OAI.ElasticityCGO.localized_formal_L2_tendsto line 342
  53. theorem OAI.ElasticityWeakLimit.bounded_weak_subsequence line 370

    Source documentation

    Bounded physical amplitudes admit a common weak subsequence in the genuine Hilbert space. For several columns, take their finite Hilbert product.

    theorem bounded_weak_subsequence [CompleteSpace H] [TopologicalSpace.SeparableSpace H]
    (u : ℕ → H) (C : ℝ) (hC : ∀ n, ‖u n‖ ≤ C) :
    ∃ w : H, ‖w‖ ≤ C ∧ ∃ σ : ℕ → ℕ, StrictMono σ ∧
      ∀ v : H, Tendsto (fun n => inner ℂ (u (σ n)) v) atTop (𝓝 (inner ℂ w v)) := by
…
  54. lemma OAI.ElasticityWeakLimit.testing_identity line 389

    Source documentation

    Weak convergence preserves any exact testing identity, including exterior agreement of the transferred amplitudes.

    lemma testing_identity {u : ℕ → H} {w : H}
    (hu : ∀ v, Tendsto (fun n => inner ℂ (u n) v) atTop (𝓝 (inner ℂ w v)))
    (v : H) (c : ℂ) (hc : ∀ n, inner ℂ (u n) v=c) : inner ℂ w v=c := by
…
  55. lemma OAI.ElasticityWeakLimit.asymptotic_testing_identity line 399

    Source documentation

    The lower-order conjugated terms vanish under weak convergence. No bound on derivatives of the sequence is required: both operators have already been transposed onto fixed test vectors.

    lemma asymptotic_testing_identity {u : ℕ → H} {w : H}
    (hu : ∀ v, Tendsto (fun n => inner ℂ (u n) v) atTop (𝓝 (inner ℂ w v)))
    (eps : ℕ → ℂ) (heps : Tendsto eps atTop (𝓝 0)) (v₁ v₂ : H)
    (heq : ∀ n, inner ℂ (u n) v₁+eps n*inner ℂ (u n) v₂=0) :
    inner ℂ w v₁=0 := by
…
  56. lemma OAI.ElasticityWeakLimit.weak_scalar line 414
  57. lemma OAI.ElasticityWeakLimit.weak_distribution line 426
  58. theorem OAI.ElasticityWeakLimit.weak_local_equation line 435

    Source documentation

    The actual distributional lower-order terms disappear after transposing to fixed tests. This is the passage used for physical transferred amplitudes.

    theorem weak_local_equation {u : ℕ → H} {w : H}
    (hu : ∀ v, Tendsto (fun n => inner ℂ (u n) v) atTop (𝓝 (inner ℂ w v)))
    (A B : H →L[ℂ] 𝓢'(E,ℂ)) (Ω : Set E) (eps : ℕ → ℂ)
    (heps : Tendsto eps atTop (𝓝 0))
    (heq : ∀ n, ElasticityRegularity.LocalEqual Ω (A (u n)+eps n • B (u n)) 0) :
    ElasticityRegularity.LocalEqual Ω (A w) 0 := by
…

    Mentions: OAI.ElasticityRegularity.LocalEqual

  59. lemma OAI.ElasticityWeakLimit.weak_local_agreement line 449
  60. lemma OAI.ElasticityDistribution.scaled_null_sum line 465
  61. lemma OAI.ElasticityDistribution.complex_smul_zero line 469
  62. theorem OAI.ElasticityDistribution.weak_physical_leading line 474

    Source documentation

    Weak physical transferred amplitudes satisfy the actual constrained leading system, not an unconstrained augmented transport.

    theorem weak_physical_leading {U : ℕ → AugHilbert} {W : AugHilbert}
    (hU : ∀ v, Tendsto (fun n => inner ℂ (U n) v) atTop (𝓝 (inner ℂ W v)))
    (Ω : Set X) (eps : ℕ → ℂ) (heps : Tendsto eps atTop (𝓝 0))
    (hne : ∀ n, eps n ≠ 0) (θ : Fin 3 → ℂ) (hθ : ∑ i, θ i*θ i=0)
    (lam m : Coeff)
    (hR : ∀ n i, LocalEq Ω (rd ((eps n)⁻¹ • θ) lam m
      (fun j => (U n j.succ : Dist)) (U n 0 : Dist) i) 0)
    (hS : ∀ n, LocalEq Ω (scd ((eps n)⁻¹ • θ) lam m
      (fun j => (U n j.succ : Dist)) (U n 0 : Dist)) 0)
    (hdiv : ∀ n, LocalEq Ω (divd ((eps n)⁻¹ • θ) (fun j => (U n j.succ : Dist)))
      (U n 0 : Dist)) :
    (∀ i, LocalEq Ω (leadingRd θ lam m (fun j => (W j.succ : Dist)) (W 0 : Dist) i) 0) ∧
…

    Mentions: OAI.ElasticityDistribution.AugHilbert, OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.LocalEq, OAI.ElasticityDistribution.rd, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.scd, OAI.ElasticityDistribution.divd, OAI.ElasticityDistribution.leadingRd

  63. theorem OAI.ElasticityWeakLimit.weak_moving_local_agreement line 527

    Source documentation

    The exterior data need only converge in distributions. In particular, this retains the finite-amplitude and correction terms of the physical CGO sequence until after the weak limit, rather than replacing them by their leading value.

    theorem weak_moving_local_agreement {u : ℕ → H} {w : H}
    (hu : ∀ v, Tendsto (fun n => inner ℂ (u n) v) atTop (𝓝 (inner ℂ w v)))
    (A : H →L[ℂ] 𝓢'(E,ℂ)) (Ω : Set E) (f : ℕ → 𝓢'(E,ℂ)) (g : 𝓢'(E,ℂ))
    (hf : ∀ φ, Tendsto (fun n => f n φ) atTop (𝓝 (g φ)))
    (heq : ∀ n, ElasticityRegularity.LocalEqual Ω (A (u n)) (f n)) :
    ElasticityRegularity.LocalEqual Ω (A w) g := by
…

    Mentions: OAI.ElasticityRegularity.LocalEqual

  64. theorem OAI.ElasticityDistribution.bounded_physical_limit line 547

    Source documentation

    Actual coefficientwise physical equations survive bounded weak extraction, including the divergence constraint and the varying physical exterior data. The bound is a premise here: deriving it from the DN transfer and its compact Carleman estimate remains separate and is not identified with the main theorem.

    theorem bounded_physical_limit
    (U : ℕ → AugHilbert) (C : ℝ) (hbound : ∀ n, ‖U n‖≤C)
    (Ω E : Set X) (eps : ℕ → ℂ) (heps : Tendsto eps atTop (𝓝 0))
    (hne : ∀ n,eps n≠0) (θ : Fin 3 → ℂ) (hθ : ∑ i,θ i*θ i=0)
    (lam m : Coeff)
    (hR : ∀ n i,LocalEq Ω (rd ((eps n)⁻¹ • θ) lam m
      (fun j => (U n j.succ : Dist)) (U n 0 : Dist) i) 0)
    (hS : ∀ n,LocalEq Ω (scd ((eps n)⁻¹ • θ) lam m
      (fun j => (U n j.succ : Dist)) (U n 0 : Dist)) 0)
    (hdiv : ∀ n,LocalEq Ω (divd ((eps n)⁻¹ • θ) (fun j => (U n j.succ : Dist)))
      (U n 0 : Dist))
    (F : ℕ → Fin 4 → Dist) (a : Fin 4 → Dist)
…

    Mentions: OAI.ElasticityDistribution.AugHilbert, OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.LocalEq, OAI.ElasticityDistribution.rd, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.scd, OAI.ElasticityDistribution.divd

  65. lemma OAI.ElasticityDistribution.augEmbed_distribution line 592
  66. theorem OAI.ElasticityDistribution.actual_augmented_equations line 599

    Source documentation

    The scalar entry of the actual augmented amplitude is its actual physical shifted divergence. Both physical equations, including the scalar consequence, are thereby inherited by the same L2 object used in weak extraction.

    theorem actual_augmented_equations {B : Set X} (z : Fin 3 → ℂ) (lam m : Coeff)
    (u : Fin 3 → SchwartzMap X ℂ)
    (hu : ∀ i,EqOn (ElasticityPhysicalAlgebra.physical z (eval lam) (eval m) u i : X → ℂ) 0 B) :
    let U := augEmbed (physicalAug z u)
…

    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityPhysicalAlgebra.physical, OAI.ElasticityDistribution.eval

  67. lemma OAI.ElasticityDistribution.actual_augmented_exterior line 624
  68. theorem OAI.ElasticityDistribution.actual_transferred_limit line 653

    Source documentation

    Weak transport extraction for the literal transferred physical sequence. The exterior leading value follows from strong convergence of the actual source augmented amplitudes, not from dropping CGO remainders by definition.

    theorem actual_transferred_limit (B K : Set X) (α β : X)
    (hθ : ∑ i,((α i : ℂ)+Complex.I*(β i : ℂ))*((α i : ℂ)+Complex.I*(β i : ℂ))=0)
    (lam m : Coeff) (h : ℕ → ℝ) (hh : Tendsto h atTop (𝓝 0)) (hne : ∀ n,h n≠0)
    (u v : ℕ → Fin 3 → SchwartzMap X ℂ) (a : Fin 4 → SchwartzMap X ℂ)
    (hv : ∀ n i,EqOn (physical (phase (h n) α β) (eval lam) (eval m) (v n) i : X → ℂ) 0 B)
    (hs : ∀ n i,tsupport (v n i-u n i : SchwartzMap X ℂ)⊆K)
    (C : ℝ) (hC : ∀ n,‖augEmbed (physicalAug (phase (h n) α β) (v n))‖≤C)
    (ha : ∀ i,Tendsto (fun n => L2 (physicalAug (phase (h n) α β) (u n) i)) atTop (𝓝 (L2 (a i)))) :
    ∃ W : AugHilbert,
      (∀ i,LocalEq B (leadingRd (fun i => (α i : ℂ)+Complex.I*(β i : ℂ)) lam m
        (fun j => (W j.succ : Dist)) (W 0 : Dist) i) 0) ∧
      LocalEq B (leadingSd (fun i => (α i : ℂ)+Complex.I*(β i : ℂ)) lam m
…

    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.eval, OAI.ElasticityDistribution.AugHilbert, OAI.ElasticityDistribution.LocalEq, OAI.ElasticityDistribution.leadingRd, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.leadingSd

  69. lemma OAI.ElasticitySequences.small_sequence line 698
  70. lemma OAI.ElasticitySequences.tendsto_of_error line 715
  71. theorem OAI.Elasticity.dn_weak_transport_column line 738

    Source documentation

    A genuine physical DN transfer yields a bounded weak leading transport column with the actual exterior leading value. Every bound and equation is derived from the physical CGO construction and the compact comparison.

    theorem dn_weak_transport_column {Ω 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)
    (hBR : B⊆Metric.ball 0 R) (α β : X) (hα : α≠0)
    (hθ : ∑ i,((α i : ℂ)+Complex.I*(β i : ℂ))*((α i : ℂ)+Complex.I*(β i : ℂ))=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)
…

    Mentions: OAI.Elasticity.X

  72. lemma OAI.ElasticitySlicing.ae_all_on_of_continuous line 813
  73. lemma OAI.ElasticitySlicing.memLp_two_slices line 832

    Source documentation

    An honest L2 function on the cylinder has L2 planar slices a.e.

    lemma memLp_two_slices {u : A × B → G} (hu : MemLp u 2 (ν.prod κ)) :
    ∀ᵐ t ∂ν, MemLp (fun z => u (t,z)) 2 κ := by
…
  74. abbrev OAI.ElasticityGeneralSlicing.PL2 line 851
  75. def OAI.ElasticityGeneralSlicing.sliceLp line 852
  76. lemma OAI.ElasticityGeneralSlicing.sliceLp_coe line 856
  77. def OAI.ElasticityGeneralSlicing.testDbar line 862
  78. def OAI.ElasticityGeneralSlicing.testGraph line 864
  79. def OAI.ElasticityGeneralSlicing.slicePair line 866
  80. lemma OAI.ElasticityGeneralSlicing.slicePair_continuous line 871
  81. lemma OAI.ElasticityGeneralSlicing.L2_test_integral line 875
  82. lemma OAI.ElasticityGeneralSlicing.slicePair_graph line 886
  83. lemma OAI.ElasticityGeneralSlicing.test_mul_integrable line 895
  84. lemma OAI.ElasticityGeneralSlicing.single_test_slice line 901

    Source documentation

    Fubini plus the fundamental lemma first gives a null set for one test.

    lemma single_test_slice {u w : P × ℂ → ℂ}
    (hu : Integrable u) (hw : Integrable w) (φ : Test)
    (he : ∀ (η : P → ℝ), ContDiff ℝ (⊤ : ℕ∞) η → HasCompactSupport η →
      (∫ q : P × ℂ, η q.1 • (φ q.2*w q-testDbar φ q.2*u q))=0) :
    ∀ᵐ t : P, ∫ z : ℂ, φ z*w (t,z)-testDbar φ z*u (t,z)=0 := by
…

    Mentions: OAI.ElasticityGeneralSlicing.testDbar

  85. theorem OAI.ElasticityGeneralSlicing.weak_slice_from_product_tests line 922

    Source documentation

    The weak cylinder equation genuinely determines the planar weak equation on a single full-measure subset of transverse parameters.

    theorem weak_slice_from_product_tests {u w : P × ℂ → ℂ}
    (hu : Integrable u) (hw : Integrable w)
    (hu2 : MemLp u 2 volume) (hw2 : MemLp w 2 volume)
    (he : ∀ (η : P → ℝ), ContDiff ℝ (⊤ : ℕ∞) η → HasCompactSupport η →
      ∀ φ : Test, (∫ q : P × ℂ,
        η q.1 • (φ q.2*w q-testDbar φ q.2*u q))=0) :
    ∀ᵐ t : P, MemLp (fun z => u (t,z)) 2 volume ∧
      MemLp (fun z => w (t,z)) 2 volume ∧
      ∀ φ : Test, (∫ z, φ z*w (t,z))=(∫ z, testDbar φ z*u (t,z)) := by
…

    Mentions: OAI.ElasticityGeneralSlicing.testDbar

  86. instance OAI.ElasticityGeneralSlicing.cylinder_temperate line 957
  87. lemma OAI.ElasticityGeneralSlicing.compact_product_test line 963
  88. def OAI.ElasticityGeneralSlicing.productTest line 972
  89. lemma OAI.ElasticityGeneralSlicing.productTest_apply line 980
  90. lemma OAI.ElasticityGeneralSlicing.productTest_deriv line 986
  91. lemma OAI.ElasticityGeneralSlicing.productTest_add line 1008
  92. lemma OAI.ElasticityGeneralSlicing.productTest_smul line 1016
  93. lemma OAI.ElasticityGeneralSlicing.productTest_dbar line 1024
  94. theorem OAI.ElasticityGeneralSlicing.cylinder_product_tests line 1033

    Source documentation

    The product-test premise of slicing is not an axiom: it follows from the actual distributional cylinder equation by an exact directional derivative.

    theorem cylinder_product_tests (u w : Lp ℂ 2 (volume : Measure (P × ℂ)))
    (hu : Integrable (u : P × ℂ → ℂ)) (hw : Integrable (w : P × ℂ → ℂ))
    (he : ∂_{((0:P),(1:ℂ))} (u : 𝓢'(P × ℂ,ℂ))+
      Complex.I • ∂_{((0:P),Complex.I)} (u : 𝓢'(P × ℂ,ℂ))+(w : 𝓢'(P × ℂ,ℂ))=0)
    (η : P → ℝ) (hη : ContDiff ℝ (⊤ : ℕ∞) η) (hcη : HasCompactSupport η) (φ : Test) :
    (∫ q : P × ℂ, η q.1 • (φ q.2*w q-testDbar φ q.2*u q))=0 := by
…

    Mentions: OAI.ElasticityGeneralSlicing.testDbar

  95. theorem OAI.ElasticityGeneralSlicing.cylinder_weak_slices line 1065

    Source documentation

    Actual weak distribution solutions on the cylinder slice to planar solutions for every compact smooth test on one full-measure parameter set.

    theorem cylinder_weak_slices (u w : Lp ℂ 2 (volume : Measure (P × ℂ)))
    (hu : Integrable (u : P × ℂ → ℂ)) (hw : Integrable (w : P × ℂ → ℂ))
    (he : ∂_{((0:P),(1:ℂ))} (u : 𝓢'(P × ℂ,ℂ))+
      Complex.I • ∂_{((0:P),Complex.I)} (u : 𝓢'(P × ℂ,ℂ))+(w : 𝓢'(P × ℂ,ℂ))=0) :
    ∀ᵐ t : P, MemLp (fun z => u (t,z)) 2 volume ∧
      MemLp (fun z => w (t,z)) 2 volume ∧
      ∀ φ : Test, (∫ z, φ z*w (t,z))=(∫ z, testDbar φ z*u (t,z)) :=
…

    Mentions: OAI.ElasticityGeneralSlicing.testDbar