OAI/Geometry/SurfaceImmersion/Primitive/PrimitiveAmplitudeParameterBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Compact C1 control of the actual inverse and square-root amplitude map. The parameter bounds are fixed before a later family is composed with it.

  1. abbrev OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PrimitiveAmplitudeData line 19
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.primitiveParameterInverse line 21
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.primitiveParameterCoefficient line 24
  4. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.primitiveParameterAmplitude line 27
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.primitiveParameterInverse_smoothAt line 30
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.primitiveParameterCoefficient_smoothAt line 36
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.primitiveParameterAmplitude_smoothAt line 45
  8. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.parameterNormData line 55
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.parameterNormData_continuousAt line 60
  10. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.compact_primitive_amplitude_C1 line 72

    Source documentation

    One neighborhood and one C1 constant control inverse operators and actual amplitudes uniformly around any compact positive family of finite data.

    theorem compact_primitive_amplitude_C1 (i : ι) {K : Set (PrimitiveAmplitudeData ι)}
    (hK : IsCompact K)
    (hgood : ∀ z ∈ K, (primitiveDataOperator z.1).IsInvertible ∧
      0 < primitiveParameterCoefficient i z) :
    ∃ eps C : ℝ, 0 < eps ∧ 1 ≤ C ∧
      ∀ z ∈ K, ∀ z' : PrimitiveAmplitudeData ι, ‖z'-z‖ < eps →
        (primitiveDataOperator z'.1).IsInvertible ∧
        0 < primitiveParameterCoefficient i z' ∧
        ‖primitiveParameterInverse z'‖ ≤ C ∧
        ‖fderiv ℝ primitiveParameterInverse z'‖ ≤ C ∧
        |primitiveParameterAmplitude i z'| ≤ C ∧
        ‖fderiv ℝ (primitiveParameterAmplitude i) z'‖ ≤ C := by
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PrimitiveAmplitudeData, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.primitiveDataOperator, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.primitiveParameterCoefficient, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.primitiveParameterInverse, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.primitiveParameterAmplitude