Conic.lean`

39 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ElasticityConic.finiteCoordinates line 13
Source documentation
Polynomial coordinates on the finite chart of the actual constrained rank-three fiber, including its scalar component.
```
def finiteCoordinates (z : ℂ) (p : Amp) : Fin 3 → ℂ :=
…
```
def OAI.ElasticityConic.finiteVector line 15
lemma OAI.ElasticityConic.finiteVector_normal line 17
lemma OAI.ElasticityConic.finiteCoordinates_vector line 22
lemma OAI.ElasticityConic.finiteVector_coordinates line 28
def OAI.ElasticityConic.finiteChart line 41
def OAI.ElasticityConic.chartZ₀ line 69
def OAI.ElasticityConic.chartZ₁ line 70
def OAI.ElasticityConic.chartTheta line 71
def OAI.ElasticityConic.chartVector line 72
def OAI.ElasticityConic.chartCoord line 74
lemma OAI.ElasticityConic.chartVector_normal line 81
lemma OAI.ElasticityConic.chartCoord_vector line 86
lemma OAI.ElasticityConic.chartVector_coord line 95
def OAI.ElasticityConic.conicChart line 115
lemma OAI.ElasticityConic.chartTheta_ne_zero line 134
lemma OAI.ElasticityConic.chartTheta_null line 138
def OAI.ElasticityAugmented.smoothEval line 150
def OAI.ElasticityAugmented.matrixEval line 153
Source documentation
Entrywise evaluation is an honest matrix ring homomorphism.
```
def matrixEval (x : X) : Matrix n n Smooth →+* Matrix n n ℂ :=
…
```
Mentions: OAI.ElasticityAugmented.X, OAI.ElasticityAugmented.Smooth
lemma OAI.ElasticityAugmented.matrixEval_apply line 155
def OAI.ElasticityAugmented.matrixD line 158
lemma OAI.ElasticityAugmented.matrixD_mul line 161
lemma OAI.ElasticityAugmented.matrixD_one line 168
lemma OAI.ElasticityAugmented.smoothMatrix_isUnit line 173

theorem OAI.ElasticityAugmented.smooth_matrix_comparison line 184

Source documentation

Smooth comparison from actual columns; only the original frame needs invertibility. Equations are initially local and preserve their real domain.

theorem smooth_matrix_comparison {B K : Set X} (hK : IsClosed K)
    (θ : Fin 3 → ℂ) (M₀ M₁ Y₀ Y₁ : Matrix n n Smooth)
    (hY : ∀ x,IsUnit (matrixEval x Y₀))
    (he₀ : ∀ x∈B,matrixEval x (matrixD θ Y₀)=matrixEval x (M₀*Y₀))
    (he₁ : ∀ x∈B,matrixEval x (matrixD θ Y₁)=matrixEval x (M₁*Y₁))
    (hs : ∀ x∉K,matrixEval x Y₁=matrixEval x Y₀) :
    ∃ G : Matrix n n Smooth,
      (∀ i j,tsupport ((G i j-(1 : Matrix n n Smooth) i j : Smooth) : X → ℂ)⊆K) ∧
      (∀ x∈B,matrixEval x (matrixD θ G)=matrixEval x (M₁*G-G*M₀)) := by
…

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

def OAI.ElasticityConic.chartMatrix line 239
lemma OAI.ElasticityConic.chartCoord_apply line 243
lemma OAI.ElasticityConic.chartCoord_deriv line 246
lemma OAI.ElasticityConic.chartCoord_2 line 251
lemma OAI.ElasticityConic.chartCoord_top line 254

lemma OAI.ElasticityConic.chart_transport_at line 267

Source documentation

The chart connection is exactly the physical normal transport, rather than a freely chosen augmented comparison equation.

lemma chart_transport_at (b : Bool) (z : ℂ) (T : Smooth) (Q p : Fin 3 → Smooth) (s : Smooth) (x : X)
    (hn : ElasticityFrame.normal (chartTheta b z) ((fun i => (p i : X → ℂ) x),(s : X → ℂ) x)=0)
    (hp : ∀ i,(direction (A := Smooth) coord (chartTheta b z) (p i) : X → ℂ) x=
…

Mentions: OAI.ElasticityFrame.normal, OAI.ElasticityConic.chartTheta

lemma OAI.ElasticityParameter.commutator_flatten line 307

theorem OAI.ElasticityParameter.matrix_holomorphic_of_supported_comparison line 322

Source documentation

The comparison equation on a holomorphic fiber chart forces holomorphy in the parameter. Nullity supplies the injective real characteristic planes; no compact-kernel or holomorphy premise for the unknown is present.

theorem matrix_holomorphic_of_supported_comparison
    (θ : Fin 3 → Smooth (X × ℂ))
    (hθx : ∀ r x z, (θ r : X × ℂ → ℂ) (x,z)=(θ r : X × ℂ → ℂ) (0,z))
    (hθ : ∀ r x, Differentiable ℂ (fun z => (θ r : X × ℂ → ℂ) (x,z)))
    (hnull : ∀ z, ∑ r, (θ r : X × ℂ → ℂ) (0,z)*(θ r : X × ℂ → ℂ) (0,z)=0)
    (hne : ∀ z, (fun r => (θ r : X × ℂ → ℂ) (0,z))≠0)
    (M₂ M₁ G : n → n → Smooth (X × ℂ))
    (hM₂ : ∀ i j x, Differentiable ℂ (fun z => (M₂ i j : X × ℂ → ℂ) (x,z)))
    (hM₁ : ∀ i j x, Differentiable ℂ (fun z => (M₁ i j : X × ℂ → ℂ) (x,z)))
    (he : ∀ i j, ∑ r, θ r*delta (basis r,0) (G i j)=
      ∑ k, (M₂ i k*G k j-G i k*M₁ k j))
    {S : Set X} (hS : IsCompact S)
…

Mentions: OAI.ElasticityParameter.Smooth, OAI.ElasticityParameter.X, OAI.ElasticityParameter.delta, OAI.ElasticityParameter.basis

lemma OAI.ElasticityAugmented.supported_matrix_eq_one line 363
lemma OAI.ElasticityAugmented.globalize_matrix_comparison line 375
lemma OAI.ElasticityAugmented.matrixD_eval line 398
theorem OAI.ElasticityAugmented.supported_matrix_unique line 406
Source documentation
The supported comparison is unique using the actual characteristic-plane compact kernel theorem, not invertibility of the transferred frame.
```
theorem supported_matrix_unique (θ : Fin 3 → ℂ) (hθ : ∑ i,θ i*θ i=0) (hne : θ≠0)
    (M₀ M₁ G H : Matrix n n Smooth)
    (heG : matrixD θ G=M₁*G-G*M₀) (heH : matrixD θ H=M₁*H-H*M₀)
    (hc : ∀ i j,HasCompactSupport ((G i j-H i j : Smooth) : X → ℂ)) : G=H := by
…
```
Mentions: OAI.ElasticityAugmented.Smooth, OAI.ElasticityAugmented.matrixD, OAI.ElasticityAugmented.X

theorem OAI.ElasticityConic.chart_frame_comparison line 455

Source documentation

Convert the actual physical rank-three fiber basis to a chart matrix; there is no assumption that the transferred columns are a basis.

theorem chart_frame_comparison {U K : Set X} (hK : IsClosed K) (hKU : K⊆U)
    (b : Bool) (z : ℂ) (T : Fin 2 → Smooth) (Q : Fin 2 → Fin 3 → Smooth)
    (p : Fin 2 → Fin 3 → Fin 3 → Smooth) (s : Fin 2 → Fin 3 → Smooth)
    (B : X → Module.Basis (Fin 3) ℂ (ElasticityFrame.Fiber (chartTheta b z)))
    (hn : ∀ q ν,normal (chartTheta b z) (p q ν)=0)
    (he : ∀ q ν x,x∈U →
      (∀ i,(direction (A := Smooth) coord (chartTheta b z) (p q ν i) : X → ℂ) x=
…

Mentions: OAI.ElasticityFrame.Fiber, OAI.ElasticityConic.chartTheta

theorem OAI.Elasticity.dn_conic_comparison line 527

Source documentation

Supported global commutator comparison on EACH conic chart, constructed from equality of the physical DN map on the original domain.

theorem dn_conic_comparison {Ω : Set X} (hΩ : IsOpen Ω) (hOB : Bornology.IsBounded Ω)
    (r₀ : ℝ) (hr₀ : 1≤r₀) (hK : closure Ω⊆Metric.closedBall 0 r₀)
    (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)) (b : Bool) (z : ℂ) :
    let k := fun q => smoothOfReal (lam q) (hl q)+smoothOfReal (m q) (hm q)
…

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