FixedMeanSubstitution.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite mean correction for one fixed operator with derivative loss. The smallness threshold is uniform in the operator; no infinite-dimensional inverse or convergence of a derivative-losing iteration is asserted.

def OAI.ClosedSurfaceR4.FiniteMean.rescaledMean line 15
lemma OAI.ClosedSurfaceR4.FiniteMean.rescaledMean_self line 19
lemma OAI.ClosedSurfaceR4.FiniteMean.rescaledMean_bounds line 24
def OAI.ClosedSurfaceR4.FiniteMean.fixedTrial line 59
Source documentation
The actual finite sequence depends only on the fixed mean operator.
```
def fixedTrial (H : E → F) (A : (E → F) → E → F) (j : ℕ) : E → F :=
…
```
lemma OAI.ClosedSurfaceR4.FiniteMean.trial_rescaledMean line 63

theorem OAI.ClosedSurfaceR4.FiniteMean.fixed_mean_substitution line 75

Source documentation

A fixed operator with an O(η) value bound and an O(η) finite-loss Lipschitz bound admits any prescribed finite number of substitutions.

theorem fixed_mean_substitution {U : Set E} (hU : UniqueDiffOn ℝ U) {s : ℝ} (hs : 0 ≤ s)
    {reference H : E → F} {r0 r1 : ℝ} (hgap : r0 < r1) {L : ℕ}
    {B K : ℕ → ℝ → ℝ} (hB : ∀ m C, 1 ≤ C → 1 ≤ B m C)
    (hK : ∀ m C, 1 ≤ C → 1 ≤ K m C)
    {C : ℕ → ℝ} (hC : ∀ m, 1 ≤ C m) (hH : ContDiffOn ℝ ∞ H U)
    (hH0 : ∀ p ∈ U, ‖H p - reference p‖ ≤ r0)
    (hbH : ∀ m, WeightedBound U s m (C m) H) (n : ℕ) :
    ∃ η0 : ℝ, 0 < η0 ∧ η0 ≤ 1 ∧ ∀ η, 0 < η → η ≤ η0 →
      ∀ A : (E → F) → E → F,
      (∀ f, ContDiffOn ℝ ∞ f U → InTrialBall U reference r1 f → ContDiffOn ℝ ∞ (A f) U) →
      (∀ m C f, 1 ≤ C → ContDiffOn ℝ ∞ f U → InTrialBall U reference r1 f →
        WeightedBound U s (m + L) C f → WeightedBound U s m (η * B m C) (A f)) →
…

Mentions: OAI.ClosedSurfaceR4.FiniteMean.InTrialBall