OAI/Geometry/SurfaceImmersion/Correction/WeightedPolynomialBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.WeightedEstimates.weightedBound_const line 16
2. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.smul_real line 26
3. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.mul_real line 36

   Distinct definitions of this name: OAI/Geometry/Immersion/ClosedSurface/MetricTensors.lean:145 (different declaration text), OAI/Geometry/SurfaceImmersion/Atlas/WeightedRealAlgebra.lean:12 (different declaration text). Qualify references as OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.mul_real@path.

4. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.finset_prod line 45

   Source documentation

   A finite product pays only the sum of the factor losses in the scale.

   lemma WeightedBound.finset_prod {ι : Type*} {U : Set A} (hU : UniqueDiffOn ℝ U)
       {s : ℝ} {m : ℕ} (hs : 0 ≤ s) (a : Finset ι) (C : ι → ℝ) (f : ι → A → ℝ)
       (hC : ∀ i ∈ a, 0 ≤ C i) (hf : ∀ i ∈ a, ContDiffOn ℝ ∞ (f i) U)
       (hb : ∀ i ∈ a, WeightedBound U s m (C i) (f i)) :
       WeightedBound U s m ((2 ^ m) ^ a.card * ∏ i ∈ a, C i) (fun x => ∏ i ∈ a, f i x) := by
   …

   Mentions: OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound

5. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.finset_prod_losses line 68
6. lemma OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound.finset_sum_losses line 82

   Source documentation

   A common loss bound for a finite polynomial is the maximum of the monomial losses, independent of the number of output derivatives.

   lemma WeightedBound.finset_sum_losses {ι : Type*} {U : Set A} (hU : UniqueDiffOn ℝ U)
       {s : ℝ} {m p : ℕ} (hs : 0 < s) (hs1 : s ≤ 1) (a : Finset ι)
       (C : ι → ℝ) (loss : ι → ℕ) (f : ι → A → E)
       (hC : ∀ i ∈ a, 0 ≤ C i) (hp : ∀ i ∈ a, loss i ≤ p)
       (hf : ∀ i ∈ a, ContDiffOn ℝ ∞ (f i) U)
       (hb : ∀ i ∈ a, WeightedBound U s m (C i / s ^ loss i) (f i)) :
       WeightedBound U s m ((∑ i ∈ a, C i) / s ^ p) (fun x => ∑ i ∈ a, f i x) := by
   …

   Mentions: OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound