OAI/MathematicalPhysics/Elasticity/Holomorphy.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElasticityPlanar.test_equation_distribution line 13
  2. theorem OAI.ElasticityPlanar.classical_parameter_smooth line 30

    Source documentation

    Uniqueness identifies the independently supplied smooth slices with the jointly smooth selection; smooth parameter dependence is a conclusion.

    theorem classical_parameter_smooth {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)
    (u : P → n → Test) (hu : ∀ p i,tsupport (u p i : ℂ → ℂ)⊆S)
    (he : ∀ p i z,schwartzDbar (toSchwartz (u p i)) z+
      ∑ j,a i j (p,z)*u p j z=f i (p,z)) :
    ∀ i,ContDiff ℝ (⊤ : ℕ∞) (fun q : P × ℂ => u q.1 i q.2) := by
…

    Mentions: OAI.ElasticityPlanar.Test, OAI.ElasticityPlanar.schwartzDbar, OAI.ElasticityPlanar.toSchwartz

  3. lemma OAI.ElasticityCoordinates.compact_parameter_identity line 79
  4. lemma OAI.ElasticityCoordinates.uniform_plane_support line 101

    Source documentation

    Uniform properness of an injective family of characteristic planes on a compact parameter set. This supplies a fixed planar support for parameter inversion, rather than silently treating moving planes as fixed.

    lemma uniform_plane_support {T : Set P} (hT : IsCompact T)
    (J : P → ℂ →L[ℝ] E) (hJ : Continuous J) (hinj : ∀ p∈T,Function.Injective (J p))
    (x : P → E) (hx : Continuous x) {K : Set E} (hK : IsCompact K) :
    ∃ S : Set ℂ,IsCompact S ∧ ∀ p∈T,∀ w,x p+J p w∈K → w∈S := by
…
  5. theorem OAI.ElasticityPlanar.moving_plane_parameter_smooth line 155

    Source documentation

    Joint smoothness from supported transport on moving characteristic planes. Neither continuity nor parameter differentiability of the unknown is assumed.

    theorem moving_plane_parameter_smooth (J : P → ℂ →L[ℝ] E)
    (hJ : ContDiff ℝ (⊤ : ℕ∞) J) (hJi : ∀ p,Function.Injective (J p))
    {S K : Set E} (hS : IsCompact S) (hK : IsCompact K)
    (a : n → n → E × P → ℂ) (ha : ∀ i j,ContDiff ℝ (⊤ : ℕ∞) (a i j))
    (has : ∀ i j x p,x∉K → a i j (x,p)=0)
    (f : n → E × P → ℂ) (hf : ∀ i,ContDiff ℝ (⊤ : ℕ∞) (f i))
    (hfs : ∀ i x p,x∉K → f i (x,p)=0)
    (u : P → n → E → ℂ) (hu : ∀ p i,ContDiff ℝ (⊤ : ℕ∞) (u p i))
    (hus : ∀ p i,tsupport (u p i)⊆S)
    (he : ∀ p i x,fderiv ℝ (u p i) x (J p 1)+Complex.I*fderiv ℝ (u p i) x (J p Complex.I)+
      ∑ j,a i j (x,p)*u p j x=f i (x,p)) :
    ∀ i,ContDiff ℝ (⊤ : ℕ∞) (fun q : E × P => u q.2 i q.1) := by
…
  6. lemma OAI.ElasticityAugmented.characteristicPlane_smooth line 223
  7. theorem OAI.ElasticityAugmented.supported_matrix_smooth line 234

    Source documentation

    Joint smoothness of the actual supported comparison. Continuity in the conic parameter is not supplied as data.

    theorem supported_matrix_smooth (θ : Fin 3 → ℂ → ℂ)
    (hθ : ∀ i,ContDiff ℝ (⊤ : ℕ∞) (θ i))
    (hnull : ∀ z,∑ i,θ i z*θ i z=0) (hne : ∀ z,(fun i => θ i z)≠0)
    (M₀ M₁ G : ℂ → Matrix n n Smooth)
    (hM₀ : ∀ i j,ContDiff ℝ (⊤ : ℕ∞) (fun q : X × ℂ => (M₀ q.2 i j : X → ℂ) q.1))
    (hM₁ : ∀ i j,ContDiff ℝ (⊤ : ℕ∞) (fun q : X × ℂ => (M₁ q.2 i j : X → ℂ) q.1))
    {S : Set X} (hS : IsCompact S) (χ : Smooth) (hχ : HasCompactSupport (χ : X → ℂ))
    (hχ1 : ∀ x∈S,(χ : X → ℂ) x=1)
    (hs : ∀ z i j,tsupport ((G z i j-(1 : Matrix n n Smooth) i j : Smooth) : X → ℂ)⊆S)
    (hMe : ∀ z x,x∉S → matrixEval x (M₀ z)=matrixEval x (M₁ z))
    (he : ∀ z,matrixD (fun i => θ i z) (G z)=M₁ z*G z-G z*M₀ z) :
    ∀ i j,ContDiff ℝ (⊤ : ℕ∞) (fun q : X × ℂ => (G q.2 i j : X → ℂ) q.1) := by
…

    Mentions: OAI.ElasticityAugmented.Smooth, OAI.ElasticityAugmented.X, OAI.ElasticityAugmented.S, OAI.ElasticityAugmented.matrixEval, OAI.ElasticityAugmented.matrixD

  8. structure OAI.ElasticityConic.JointHolomorphic line 326
  9. lemma OAI.ElasticityConic.JointHolomorphic.fixed line 330
  10. lemma OAI.ElasticityConic.JointHolomorphic.param line 332
  11. lemma OAI.ElasticityConic.JointHolomorphic.const line 334
  12. lemma OAI.ElasticityConic.JointHolomorphic.add line 336
  13. lemma OAI.ElasticityConic.JointHolomorphic.sub line 338
  14. lemma OAI.ElasticityConic.JointHolomorphic.mul line 340
  15. lemma OAI.ElasticityConic.JointHolomorphic.pow line 342
  16. lemma OAI.ElasticityConic.JointHolomorphic.sum line 344
  17. lemma OAI.ElasticityConic.chartZ₀_regular line 349
  18. lemma OAI.ElasticityConic.chartZ₁_regular line 353
  19. lemma OAI.ElasticityConic.chartTheta_regular line 357
  20. lemma OAI.ElasticityConic.h₁_regular line 362
  21. lemma OAI.ElasticityConic.h₂_regular line 367
  22. lemma OAI.ElasticityConic.direction_regular line 372
  23. lemma OAI.ElasticityConic.thetaGamma_regular line 376
  24. lemma OAI.ElasticityConic.transportT_regular line 380
  25. lemma OAI.ElasticityConic.transportQ_regular line 385
  26. lemma OAI.ElasticityConic.chartMatrix_regular line 397

    Source documentation

    These are the literal chart coefficients, jointly smooth and holomorphic in the normalized conic direction, with the physical point fixed.

    lemma chartMatrix_regular (b : Bool) (T : ℂ → Smooth) (Q : ℂ → Fin 3 → Smooth)
    (hT : JointHolomorphic (fun q : X × ℂ => (T q.2 : X → ℂ) q.1))
    (hQ : ∀ i,JointHolomorphic (fun q : X × ℂ => (Q q.2 i : X → ℂ) q.1)) (i j : Fin 3) :
    JointHolomorphic (fun q : X × ℂ => (chartMatrix b q.2 (T q.2) (Q q.2) i j : X → ℂ) q.1) := by
…

    Mentions: OAI.ElasticityConic.JointHolomorphic, OAI.ElasticityConic.chartMatrix

  27. theorem OAI.ElasticityAugmented.supported_matrix_holomorphic line 422

    Source documentation

    Both regularity statements are derived for a separately constructed family from its transport equation and ONE fixed spatial support.

    theorem supported_matrix_holomorphic (θ : Fin 3 → ℂ → ℂ)
    (hθs : ∀ i,ContDiff ℝ (⊤ : ℕ∞) (θ i)) (hθh : ∀ i,Differentiable ℂ (θ i))
    (hnull : ∀ z,∑ i,θ i z*θ i z=0) (hne : ∀ z,(fun i => θ i z)≠0)
    (M₀ M₁ G : ℂ → Matrix n n Smooth)
    (hM₀ : ∀ i j,ElasticityConic.JointHolomorphic (fun q : X × ℂ => (M₀ q.2 i j : X → ℂ) q.1))
    (hM₁ : ∀ i j,ElasticityConic.JointHolomorphic (fun q : X × ℂ => (M₁ q.2 i j : X → ℂ) q.1))
    {S : Set X} (hS : IsCompact S) (χ : Smooth) (hχ : HasCompactSupport (χ : X → ℂ))
    (hχ1 : ∀ x∈S,(χ : X → ℂ) x=1)
    (hs : ∀ z i j,tsupport ((G z i j-(1 : Matrix n n Smooth) i j : Smooth) : X → ℂ)⊆S)
    (hMe : ∀ z x,x∉S → matrixEval x (M₀ z)=matrixEval x (M₁ z))
    (he : ∀ z,matrixD (fun i => θ i z) (G z)=M₁ z*G z-G z*M₀ z) :
    ∀ i j,ElasticityConic.JointHolomorphic (fun q : X × ℂ => (G q.2 i j : X → ℂ) q.1) := by
…

    Mentions: OAI.ElasticityAugmented.Smooth, OAI.ElasticityConic.JointHolomorphic, OAI.ElasticityAugmented.X, OAI.ElasticityAugmented.S, OAI.ElasticityAugmented.matrixEval, OAI.ElasticityAugmented.matrixD