CommonExterior.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ElasticityBoundary.extension_jets line 14

theorem OAI.ElasticityBoundary.common_exterior_of_all_jets line 20

Source documentation

Once actual boundary jets have been determined, the source common exterior reduction follows, including every bounded component of the exterior.

theorem common_exterior_of_all_jets {Ω U₁ U₂ : Set E} (hc : IsCompact (closure Ω))
    (hU₁ : IsOpen U₁) (hU₂ : IsOpen U₂) (h₁ : closure Ω⊆U₁) (h₂ : closure Ω⊆U₂)
    (l₁ m₁ l₂ m₂ : E → ℝ)
    (hl₁ : ContDiffOn ℝ (⊤ : ℕ∞) l₁ U₁) (hm₁ : ContDiffOn ℝ (⊤ : ℕ∞) m₁ U₁)
    (hl₂ : ContDiffOn ℝ (⊤ : ℕ∞) l₂ U₂) (hm₂ : ContDiffOn ℝ (⊤ : ℕ∞) m₂ U₂)
    (hp₁ : ∀ x∈closure Ω, 0 < m₁ x ∧ 0 < 3*l₁ x+2*m₁ x)
    (hp₂ : ∀ x∈closure Ω, 0 < m₂ x ∧ 0 < 3*l₂ x+2*m₂ x)
    (hjl : ∀ n : ℕ, ∀ x∈frontier Ω, iteratedFDeriv ℝ n l₂ x=iteratedFDeriv ℝ n l₁ x)
    (hjm : ∀ n : ℕ, ∀ x∈frontier Ω, iteratedFDeriv ℝ n m₂ x=iteratedFDeriv ℝ n m₁ x) :
    ∃ L₁ M₁ L₂ M₂ : E → ℝ,
      ContDiff ℝ (⊤ : ℕ∞) L₁ ∧ ContDiff ℝ (⊤ : ℕ∞) M₁ ∧
      ContDiff ℝ (⊤ : ℕ∞) L₂ ∧ ContDiff ℝ (⊤ : ℕ∞) M₂ ∧
…

def OAI.Elasticity.BoundaryJetDetermination line 89
lemma OAI.Elasticity.Admissible.common_neighborhood line 96
lemma OAI.Elasticity.admissible_of_global line 104

theorem OAI.Elasticity.admissible_common_exterior_of_jets line 113

Source documentation

The extension and DN-localization part of the boundary reduction is fully proved. The all-jet premise here is explicitly the still-missing boundary input; this declaration is NOT the main inverse theorem.

theorem admissible_common_exterior_of_jets {Ω : Set X} (hD : Domain Ω)
    (l₁ m₁ l₂ m₂ : X → ℝ) (ha₁ : Admissible Ω l₁ m₁) (ha₂ : Admissible Ω l₂ m₂)
    (hjl : ∀ n : ℕ,∀ x∈frontier Ω,iteratedFDeriv ℝ n l₂ x=iteratedFDeriv ℝ n l₁ x)
    (hjm : ∀ n : ℕ,∀ x∈frontier Ω,iteratedFDeriv ℝ n m₂ x=iteratedFDeriv ℝ n m₁ x)
    (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₁ Ωᶜ ∧
…

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