ManufacturedTransport.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual manufactured fields admit transport maps with common C4 and inverse Lipschitz constants, chosen before the instance.

theorem OAI.ContinuumCoulomb.manufactured_transport_family_with_charge line 13

theorem OAI.ContinuumCoulomb.manufactured_transport_family line 55

Source documentation

The original flow interface, retaining the same fixed constants.

theorem manufactured_transport_family (hpublished : PublishedC4FlowInput) :
    ∃ rho : ℕ, 0 < rho ∧ ∃ L K : ℝ≥0, 0 < L ∧ 0 < K ∧
      ∀ (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) →
      ∃ G : Position → ℝ → Position,
        IsUnitTimeFlow (moserVelocity rho (manufacturedWellField freq scale S u)) G ∧
        Function.Bijective (fun x => G x 1) ∧
        LipschitzWith L (fun x => G x 1) ∧ AntilipschitzWith K (fun x => G x 1) ∧
        (∀ x, x ∉ tsupport (manufacturedWellField freq scale S u) → G x 1 = x) ∧
        ContDiff ℝ 4 (fun x => G x 1) ∧
…

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