OAI/Geometry/SurfaceImmersion/Correction/UniformRealModeCoefficients.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform reconstruction estimates on a fixed compact set of real two-jets.

  1. def OAI.ClosedSurfaceR4.SmallModes.admissibleComplexJets line 13
  2. lemma OAI.ClosedSurfaceR4.SmallModes.admissibleComplexJets_domain line 17
  3. def OAI.ClosedSurfaceR4.SmallModes.complexifyJetCLM line 28
  4. def OAI.ClosedSurfaceR4.SmallModes.complexifyJetLI line 31
  5. lemma OAI.ClosedSurfaceR4.SmallModes.complexifyJet_mem line 42
  6. lemma OAI.ClosedSurfaceR4.SmallModes.twoJet_complexify line 55
  7. theorem OAI.ClosedSurfaceR4.SmallModes.compact_real_reconstruction_bounds line 86

    Source documentation

    The constant precedes the map and scale. Its only geometric input is a fixed compact set of admissible real two-jets; higher bounds enter polynomially.

    theorem compact_real_reconstruction_bounds {U : Set Base} (hU : IsOpen U)
    {Ω K : Set RealTwoJet} (hΩ : RealJetDomain Ω) (hK : IsCompact K) (hKΩ : K ⊆ Ω)
    (m : ℕ) :
    ∃ D : ℝ, 1 ≤ D ∧ ∀ (F : RField 4) (s C : ℝ), 0 < s → 1 ≤ C →
      ContDiff ℝ ∞ F → MapsTo (realTwoJet F) U K →
      WeightedBound U s m C (realTwoJet F) →
      ReconstructionCoefficientBound (fun p => complexify (F p)) U s m
        ((m.factorial : ℝ) * D * C^m) := by
…

    Mentions: OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.SmallModes.ReconstructionCoefficientBound