OAI/Geometry/SurfaceImmersion/Atlas/PhaseBasisPerturbation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Actual coefficient forms for nearby phase covectors. The inverse operator constructs the new decomposition and preserves compact positive cone margins.

  1. def OAI.ClosedSurfaceR4.PhaseGeometry.perturbedPhaseOperator line 15
  2. lemma OAI.ClosedSurfaceR4.PhaseGeometry.perturbedPhaseOperator_apply line 19
  3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.perturbedPhaseOperator_self line 24
  4. lemma OAI.ClosedSurfaceR4.PhaseGeometry.perturbedPhaseOperator_smooth line 30
  5. def OAI.ClosedSurfaceR4.PhaseGeometry.perturbedPhaseCoefficient line 40
  6. lemma OAI.ClosedSurfaceR4.PhaseGeometry.perturbedPhaseCoefficient_self line 44
  7. lemma OAI.ClosedSurfaceR4.PhaseGeometry.perturbedPhase_decomposition line 49
  8. lemma OAI.ClosedSurfaceR4.PhaseGeometry.perturbedPhaseCoefficient_smoothAt line 57
  9. def OAI.ClosedSurfaceR4.PhaseGeometry.positivePhaseParameters line 63
  10. lemma OAI.ClosedSurfaceR4.PhaseGeometry.positivePhaseParameters_open line 67
  11. theorem OAI.ClosedSurfaceR4.PhaseGeometry.compact_positive_phase_perturbation line 89

    Source documentation

    Nearby covectors admit actual smooth inverse coefficient forms, positive uniformly over the fixed compact collection of target tensor values.

    theorem compact_positive_phase_perturbation (P : PhaseBasis) {K : Set PhaseMean.Tensor}
    (hK : IsCompact K) (hpos : ∀ H ∈ K, ∀ i, 0 < P.Q i H) :
    ∃ eps : ℝ, 0 < eps ∧ ∀ xi : Fin 3 → Base, ‖xi-P.ξ‖ < eps →
      (perturbedPhaseOperator P xi).IsInvertible ∧ (∀ i, xi i ≠ 0) ∧
        ∀ H ∈ K, ∀ i, 0 < perturbedPhaseCoefficient P xi i H := by
…

    Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.PhaseBasis, OAI.ClosedSurfaceR4.PhaseMean.Tensor, OAI.ClosedSurfaceR4.PhaseGeometry.perturbedPhaseOperator, OAI.ClosedSurfaceR4.PhaseGeometry.perturbedPhaseCoefficient