PhaseMeanDomains.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Compact good geometry supplies the open domains and strict coefficient margins needed by the actual local mean construction.

theorem OAI.ClosedSurfaceR4.PhaseGeometry.compact_good_phase_neighborhood line 16

theorem OAI.ClosedSurfaceR4.PhaseGeometry.compact_phase_mean_domains line 38

Source documentation

The three phases share positive trial and coefficient radii. All domains and radii are chosen from the fixed compact reference geometry.

theorem compact_phase_mean_domains {F : RField 4} (hF : ContDiff ℝ ∞ F)
    (K : Compacts Base) (hImm : ∀ x ∈ (K : Set Base), Function.Injective (fderiv ℝ F x))
    (ξ : Fin 3 → Base)
    (hgood : ∀ j x, x ∈ (K : Set Base) → Good (realSecondTensor F x) (ξ j))
    (Q : Fin 3 → PhaseMean.Tensor →L[ℝ] ℝ) (H : Base → PhaseMean.Tensor) (hH : Continuous H)
    (hpos : ∀ j x, x ∈ (K : Set Base) → 0 < Q j (H x)) :
    ∃ r ρ R : ℝ, 0 < r ∧ 0 < ρ ∧ 0 < R ∧
      ∃ U K₁ Ω : Fin 3 → Set Base,
        (∀ j, IsOpen (U j)) ∧ (∀ j, IsCompact (K₁ j)) ∧ (∀ j, IsOpen (Ω j)) ∧
        (∀ j, (K : Set Base) ⊆ U j) ∧ (∀ j, U j ⊆ K₁ j) ∧ (∀ j, K₁ j ⊆ Ω j) ∧
        (∀ j x, x ∈ Ω j → Function.Injective (fderiv ℝ F x) ∧
          Good (realSecondTensor F x) (ξ j)) ∧
…

Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.Good, OAI.ClosedSurfaceR4.PhaseMean.Tensor

theorem OAI.ClosedSurfaceR4.PhaseGeometry.compact_phase_original_domain line 87
Source documentation
The original-coordinate coefficient domain can always be chosen open and bounded while containing the compact phase support.
```
theorem compact_phase_original_domain (K : Compacts Base) :
    ∃ (U₀ : Set JetPolynomial.Base) (K₀ : Compacts JetPolynomial.Base),
      IsOpen U₀ ∧ U₀ ⊆ K₀ ∧
      (JetPolynomial.Perturbation.jetSupport K : Set JetPolynomial.Base) ⊆ U₀ := by
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.jetSupport