Recovery.lean`

61 declarations, 0 contain sorry, 0 declared as axioms

Finite-type uniqueness used in the last step of the elasticity proof. All spaces and coefficient fields below are actual functions, not axioms.

abbrev OAI.ElasticityConic.C3 line 11
abbrev OAI.ElasticityConic.Mat3 line 12
def OAI.ElasticityConic.null line 14
def OAI.ElasticityConic.theta line 16
def OAI.ElasticityConic.h₁ line 19
def OAI.ElasticityConic.h₂ line 20
lemma OAI.ElasticityConic.dot3 line 22
lemma OAI.ElasticityConic.theta_null line 25
lemma OAI.ElasticityConic.theta_dot_h₁ line 30
lemma OAI.ElasticityConic.theta_dot_h₂ line 35
lemma OAI.ElasticityConic.theta_eq line 40
lemma OAI.ElasticityConic.theta_ne_zero line 44
lemma OAI.ElasticityConic.null_dot_zero line 55
Source documentation
The concrete spanning assertion used twice in the source proof.
```
lemma null_dot_zero (v : C3)
    (hv : ∀ θ : C3, θ ≠ 0 → null θ → dotProduct θ v = 0) : v = 0 := by
…
```
Mentions: OAI.ElasticityConic.C3, OAI.ElasticityConic.null
theorem OAI.ElasticityConic.scalar_of_null_annihilator line 73
Source documentation
Null directions used to test the entire ambient matrix, without an analytic argument on projective space. These imply precisely (scalar-ambient-difference).
```
theorem scalar_of_null_annihilator (K : Mat3)
    (hK : ∀ θ : C3, θ ≠ 0 → null θ →
      ∀ p : C3, dotProduct θ p = 0 → dotProduct (K *ᵥ θ) p = 0) :
    ∃ κ : ℂ, K = κ • (1 : Mat3) := by
…
```
Mentions: OAI.ElasticityConic.Mat3, OAI.ElasticityConic.C3, OAI.ElasticityConic.null
theorem OAI.ElasticityFiniteType.zero_of_homogeneous_system line 128
def OAI.ElasticityFiniteType.D line 163
Source documentation
Constant-direction differentiation. All directions are real; the values may be real or complex, as in the source lemma.
```
def D (f : E → F) (v : E) : E → F := fun x => fderiv ℝ f x v
```
lemma OAI.ElasticityFiniteType.contDiff_D line 165
lemma OAI.ElasticityFiniteType.D_D line 169
lemma OAI.ElasticityFiniteType.D_comm line 177
lemma OAI.ElasticityFiniteType.D_add line 185
lemma OAI.ElasticityFiniteType.D_mul line 190
lemma OAI.ElasticityFiniteType.D_sum line 195
def OAI.ElasticityFiniteType.matrixCLM line 205
lemma OAI.ElasticityFiniteType.matrixCLM_apply line 208
def OAI.ElasticityFiniteType.coordL line 212
def OAI.ElasticityFiniteType.systemCLM line 215
lemma OAI.ElasticityFiniteType.systemCLM_basis line 220
lemma OAI.ElasticityFiniteType.continuous_systemCLM line 226

theorem OAI.ElasticityFiniteType.zero_of_coordinate_system line 240

Source documentation

Coordinate form of the homogeneous-system uniqueness statement.

theorem zero_of_coordinate_system (b : Basis ι ℝ E)
    {f : E → κ → ℝ} {M : E → ι → κ → κ → ℝ}
    (hf : Differentiable ℝ f)
    (hM : ∀ s a c, Continuous (fun x => M x s a c))
    (hsystem : ∀ x s a, fderiv ℝ f x (b s) a = ∑ c, M x s a c * f x c)
    {x₀ : E} (hzero : f x₀ = 0) : ∀ x, f x = 0 := by
…

def OAI.ElasticityFiniteType.C line 262
def OAI.ElasticityFiniteType.d line 266
theorem OAI.ElasticityFiniteType.finite_type_closure line 269
lemma OAI.ElasticityFiniteType.contDiff_C line 317
lemma OAI.ElasticityFiniteType.contDiff_d line 326

theorem OAI.ElasticityFiniteType.finite_type_zero line 334

Source documentation

The precise global finite-type endpoint needed after taking the common exterior extensions. The index type has at least two elements, so there is a non-diagonal Hessian entry for each direction.

theorem finite_type_zero [FiniteDimensional ℝ E] [Nontrivial ι]
    (e : Basis ι ℝ E) {η q : E → ℝ} {B : ι → ι → ι → E → ℝ}
    (hη : ContDiff ℝ (⊤ : ℕ∞) η) (hq : ContDiff ℝ (⊤ : ℕ∞) q)
    (hB : ∀ i j a, ContDiff ℝ (⊤ : ℕ∞) (B i j a))
    (hess : ∀ i j, D (D η (e i)) (e j) =
      fun x => ∑ a, B i j a x * D η (e a) x + if i = j then q x else 0)
    {W : Set E} (hW : IsOpen W) (hne : W.Nonempty) (hz : ∀ x ∈ W, η x = 0) :
    (∀ x, η x = 0) ∧ (∀ x, q x = 0) := by
…

Mentions: OAI.ElasticityFiniteType.D

abbrev OAI.ElasticityRecovery.X line 417
abbrev OAI.ElasticityRecovery.RMat line 418
def OAI.ElasticityRecovery.basis line 420
def OAI.ElasticityRecovery.grad line 422
def OAI.ElasticityRecovery.hessian line 424
def OAI.ElasticityRecovery.dir line 427
lemma OAI.ElasticityRecovery.D_sub line 430
lemma OAI.ElasticityRecovery.grad_sub line 435
lemma OAI.ElasticityRecovery.dir_sub line 439
lemma OAI.ElasticityRecovery.fderiv_zero_of_null line 443
lemma OAI.ElasticityRecovery.zero_of_null_derivatives line 453
lemma OAI.ElasticityRecovery.real_scalar_of_null_annihilator line 461
def OAI.ElasticityRecovery.QMatrix line 474
Source documentation
Real matrix whose null contraction is exactly the Q block.
```
def QMatrix (m k : X → ℝ) (x : X) : RMat := fun i j =>
…
```
Mentions: OAI.ElasticityRecovery.X, OAI.ElasticityRecovery.RMat
def OAI.ElasticityRecovery.T line 480
def OAI.ElasticityRecovery.Q line 483
def OAI.ElasticityRecovery.EqualRestrictedTransports line 488
Source documentation
This is equality of the two restricted bottom rows, not a DN hypothesis. Deriving it from the actual DN maps is still required by the full theorem.
```
def EqualRestrictedTransports (m₁ k₁ m₂ k₂ : X → ℝ) : Prop :=
…
```
Mentions: OAI.ElasticityRecovery.X
lemma OAI.ElasticityRecovery.contDiff_log line 494
lemma OAI.ElasticityRecovery.contDiff_logRatio line 499
lemma OAI.ElasticityRecovery.ratio_equal line 506
lemma OAI.ElasticityRecovery.ratios_algebra line 531
lemma OAI.ElasticityRecovery.hessian_sub line 544
lemma OAI.ElasticityRecovery.contDiff_grad line 553
lemma OAI.ElasticityRecovery.contDiff_hessian line 556
lemma OAI.ElasticityRecovery.contDiff_QMatrix line 559
lemma OAI.ElasticityRecovery.recovery_entry line 571

theorem OAI.ElasticityRecovery.coefficients_equal_of_restricted_transports line 585

Source documentation

The final coefficient-recovery step, with its genuine intermediate transport hypothesis explicit. This is not the main DN uniqueness theorem.

theorem coefficients_equal_of_restricted_transports
    {m₁ k₁ m₂ k₂ : X → ℝ}
    (hm₁ : ContDiff ℝ (⊤ : ℕ∞) m₁) (hk₁ : ContDiff ℝ (⊤ : ℕ∞) k₁)
    (hm₂ : ContDiff ℝ (⊤ : ℕ∞) m₂) (hk₂ : ContDiff ℝ (⊤ : ℕ∞) k₂)
    (hmp₁ : ∀ x, 0 < m₁ x) (hkp₁ : ∀ x, 0 < k₁ x)
    (hmp₂ : ∀ x, 0 < m₂ x) (hkp₂ : ∀ x, 0 < k₂ x)
    (ht : EqualRestrictedTransports m₁ k₁ m₂ k₂)
    {W : Set X} (hW : IsOpen W) (hne : W.Nonempty)
    (hmW : ∀ x ∈ W, m₁ x = m₂ x) (hkW : ∀ x ∈ W, k₁ x = k₂ x) :
    m₁ = m₂ ∧ k₁ = k₂ := by
…

Mentions: OAI.ElasticityRecovery.X, OAI.ElasticityRecovery.EqualRestrictedTransports