OAI/Geometry/SurfaceImmersion/Correction/FiniteMetricPolynomial.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.PeriodicExpansion.vectorPolynomialValue line 14
2. def OAI.ClosedSurfaceR4.PeriodicExpansion.metricPolynomial line 17
3. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.metricPolynomial_eval line 21
4. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.metricPolynomial_coeff line 36

   Source documentation

   At each degree no larger than the vector degree, the usual convolution contains every contributing term, with no truncation at either end.

   lemma metricPolynomial_coeff {n r : ℕ} (hr : r ≤ n) (a b : ℕ → E) :
       (metricPolynomial n a b).coeff r =
         ∑ i ∈ Finset.range (r + 1), inner ℝ (a i) (b (r - i)) := by
   …

   Mentions: OAI.ClosedSurfaceR4.PeriodicExpansion.metricPolynomial

5. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.metricPolynomial_coeff_pos line 80
6. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.metricPolynomial_degree line 89
7. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.metricPolynomial_expansion line 103

   Source documentation

   Split the exact metric polynomial at any chosen expansion order.

   lemma metricPolynomial_expansion (n k : ℕ) (hk : k ≤ 2 * n + 1)
       (a b : ℕ → E) (z : ℝ) :
       inner ℝ (vectorPolynomialValue n a z) (vectorPolynomialValue n b z) =
         (∑ i ∈ Finset.range k, (metricPolynomial n a b).coeff i * z ^ i) +
         ∑ i ∈ Finset.Ico k (2 * n + 1), (metricPolynomial n a b).coeff i * z ^ i := by
   …

   Mentions: OAI.ClosedSurfaceR4.PeriodicExpansion.vectorPolynomialValue, OAI.ClosedSurfaceR4.PeriodicExpansion.metricPolynomial