OAI/Geometry/SurfaceImmersion/Correction/TensorAtlasMean.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The global nonlinear mean is the finite restoration of the actual local means evaluated on unweighted chart readings.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasMean line 29
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasMean_symmetric line 34
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasMean_sub line 40
  4. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorReadBallConstant line 49

    Source documentation

    The atlas-only enlargement needed when a global encoded tensor ball is read in any one chart. It is independent of reference tensors and all orders.

    def tensorReadBallConstant : ℝ := Classical.choose A.tensorPlaneRead_decode_ball
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.one_le_tensorReadBallConstant line 51
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorReadBallConstant_ball line 54
  7. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorTrialRadius line 66

    Source documentation

    A fixed global trial radius for a prescribed local geometric margin.

    def tensorTrialRadius (r₁ : ℝ) : ℝ := r₁/(2*A.tensorReadBallConstant)
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorTrialRadius_pos line 68
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorReadBallConstant_mul_trialRadius line 72
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorTrialRadius_margin line 79
  11. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasMean_majorants_fixed_ball line 86

    Source documentation

    Fixed atlas constants turn local value and difference estimates into exactly the hypotheses used by finite global mean substitution.

    theorem atlasMean_majorants_fixed_ball
    (reference : ∀ x : M, CovariantTwoTensor x)
    (href : ContMDiff planeModel (planeModel.prod 𝓘(ℝ, TensorFiber)) ∞
      (fun x => TotalSpace.mk' TensorFiber x (reference x)))
    (L : ℕ) (B K : ℕ → ℝ → ℝ)
    (hB : ∀ m C, 1 ≤ C → 1 ≤ B m C) (hK : ∀ m C, 1 ≤ C → 1 ≤ K m C) :
    ∀ r : ℝ, 0 ≤ r →
      (∀ f : Base → A.centers → TensorFiber, ContDiff ℝ ∞ f →
        InTrialBall univ (A.tensorEncode reference) r f → ∀ i : A.centers,
        InTrialBall univ (A.tensorPlaneRead i reference) (A.tensorReadBallConstant*r)
          (A.tensorPlaneRead i (A.tensorDecode f))) ∧ ∃ β κ : ℕ → ℝ → ℝ,
      ∀ {s : ℝ}, 0 < s → s ≤ 1 → ∀ η : ℝ, 0 < η →
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.TensorFiber

  12. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasMean_majorants_all_radii line 180

    Source documentation

    Fixed atlas constants turn local value and difference estimates into exactly the hypotheses used by finite global mean substitution.

    theorem atlasMean_majorants_all_radii
    (reference : ∀ x : M, CovariantTwoTensor x)
    (href : ContMDiff planeModel (planeModel.prod 𝓘(ℝ, TensorFiber)) ∞
      (fun x => TotalSpace.mk' TensorFiber x (reference x)))
    (L : ℕ) (B K : ℕ → ℝ → ℝ)
    (hB : ∀ m C, 1 ≤ C → 1 ≤ B m C) (hK : ∀ m C, 1 ≤ C → 1 ≤ K m C) :
    ∃ D₀ : ℝ, 1 ≤ D₀ ∧ ∀ r : ℝ, 0 ≤ r →
      (∀ f : Base → A.centers → TensorFiber, ContDiff ℝ ∞ f →
        InTrialBall univ (A.tensorEncode reference) r f → ∀ i : A.centers,
        InTrialBall univ (A.tensorPlaneRead i reference) (D₀*r)
          (A.tensorPlaneRead i (A.tensorDecode f))) ∧ ∃ β κ : ℕ → ℝ → ℝ,
      ∀ {s : ℝ}, 0 < s → s ≤ 1 → ∀ η : ℝ, 0 < η →
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.TensorFiber

  13. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasMean_majorants line 209