Uniqueness.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ElasticityBoundaryPacket.admissible_common_exterior line 14

Source documentation

Full common-exterior reduction from the physical DN map. In particular no prior boundary jets or agreement on a boundary neighbourhood is assumed.

theorem admissible_common_exterior {Ω : Set X} (hD : SourceDomain Ω)
    (l₁ m₁ l₂ m₂ : X → ℝ) (ha₁ : Admissible Ω l₁ m₁) (ha₂ : Admissible Ω l₂ m₂)
    (hDN : DN Ω l₁ m₁=DN Ω l₂ m₂) :
    ∃ L₁ M₁ L₂ M₂ : X → ℝ,
      ContDiff ℝ (⊤ : ℕ∞) L₁ ∧ ContDiff ℝ (⊤ : ℕ∞) M₁ ∧
      ContDiff ℝ (⊤ : ℕ∞) L₂ ∧ ContDiff ℝ (⊤ : ℕ∞) M₂ ∧
      EqOn L₁ l₁ Ω ∧ EqOn M₁ m₁ Ω ∧ EqOn L₂ l₂ Ω ∧ EqOn M₂ m₂ Ω ∧
      (∀ x,0 < M₁ x ∧ 0<3*L₁ x+2*M₁ x) ∧
      (∀ x,0 < M₂ x ∧ 0<3*L₂ x+2*M₂ x) ∧
      EqOn L₂ L₁ Ωᶜ ∧ EqOn M₂ M₁ Ωᶜ ∧
      DN Ω L₁ M₁=DN Ω L₂ M₂ ∧
      ∃ K,IsCompact K ∧ ∀ x∉K,L₁ x=0 ∧ M₁ x=1 ∧ L₂ x=0 ∧ M₂ x=1 := by
…

Mentions: OAI.ElasticityBoundaryPacket.X

lemma OAI.Elasticity.exteriorConstant_of_eq_const line 45
theorem OAI.Elasticity.source_global_uniqueness line 60
Source documentation
Exact global smooth isotropic elasticity uniqueness on every bounded connected domain with genuine smooth open boundary charts. Boundary jets, common exterior, physical transfer, weak limits, constrained common frames, parameter holomorphy and transport matching are all proved dependencies.
```
theorem source_global_uniqueness (Ω : Set X) (hD : SourceDomain Ω)
    (lam₁ mu₁ lam₂ mu₂ : X → ℝ)
    (ha₁ : Admissible Ω lam₁ mu₁) (ha₂ : Admissible Ω lam₂ mu₂)
    (hDN : DN Ω lam₁ mu₁=DN Ω lam₂ mu₂) :
    (∀ x∈Ω,lam₁ x=lam₂ x) ∧ (∀ x∈Ω,mu₁ x=mu₂ x) := by
…
```
Mentions: OAI.Elasticity.X, OAI.Elasticity.SourceDomain, OAI.Elasticity.Admissible, OAI.Elasticity.DN
theorem OAI.Elasticity.global_uniqueness line 94
Distinct definitions of this name: ComparatorChallenges/ElasticityUniqueness.lean:103 (different declaration text). Qualify references as OAI.Elasticity.global_uniqueness@path.