WeightedMultilinearVariations.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Product bounds for non-normalized variation maps.

lemma OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.rescale_succ line 14
lemma OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.rescale_inverse line 18

theorem OAI.ClosedSurfaceR4.JetPolynomial.Expression.compact_multilinear_variation_bound line 28

Source documentation

Bounds for the first three actual variations, linear in each participating map bound and with a single accuracy-independent scale exponent.

theorem compact_multilinear_variation_bound {U : Set Base} {O K : Set LowJet}
    (hU : IsOpen U) (hO : IsOpen O) (hK : IsCompact K) (hKO : K ⊆ O)
    (e : Expression) (he : e.SmoothCoeffs O) (m : ℕ) (B : ℝ) (hB : 1 ≤ B) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (G : Fin 4 → Base → Space) (s : ℝ) (C : Fin 3 → ℝ),
      0 < s → s ≤ 1 → (∀ i, 0 < C i) →
      (∀ i, ContDiff ℝ ∞ (G i)) → Set.MapsTo (lowJet (G 0)) U K →
      WeightedBound U s (m + e.order) B (lowJet (G 0)) →
      (∀ i : Fin 3, WeightedBound U s (m + e.order) (C i) (G i.succ)) →
      ∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ i : Fin 3,
        WeightedBound U s m
          (D * (C 0 * (if 1 ≤ i then C 1 else 1) * (if 2 ≤ i then C 2 else 1)) /
            s ^ (e.loss + 6)) (fun p => (e.variations i).eval G (p, t)) := by
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.lowJet, OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval