ManufacturedUniformFlow.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The same integer background density and the same flow derivative constant work for every separated manufactured well family.

theorem OAI.ContinuumCoulomb.manufactured_uniform_density_and_flow line 14

Source documentation

The background density is selected before the size, sites, field scale, or slab width. Thus the published flow input has uniform constants.

theorem manufactured_uniform_density_and_flow (hpublished : PublishedC4FlowInput) :
    ∃ rho : ℕ, 0 < rho ∧ ∃ C : ℝ, 0 < C ∧
      ∀ (freq scale S : ℝ), 0 < scale → 1 ≤ S →
      ∀ (m : ℕ) (u : Fin m → PlanarPosition),
      (∀ i j, i ≠ j → 3 ≤ ‖u i-u j‖) →
      (∀ i, localizedCounterterm freq u i ≤ scale) →
      (∀ x, |manufacturedCharge (manufacturedWellField freq scale S u) x| ≤ (rho:ℝ)/2) ∧
      (∀ G : Position → ℝ → Position,
        IsUnitTimeFlow (moserVelocity rho (manufacturedWellField freq scale S u)) G →
        ∀ k : ℕ, 1 ≤ k → k ≤ 4 → ∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ x,
          ‖iteratedFDeriv ℝ k (fun y => G y t) x‖ ≤ C) := by
…

Mentions: OAI.ContinuumCoulomb.PublishedC4FlowInput, OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.localizedCounterterm, OAI.ContinuumCoulomb.manufacturedCharge, OAI.ContinuumCoulomb.manufacturedWellField, OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.IsUnitTimeFlow, OAI.ContinuumCoulomb.moserVelocity