Gluing on the actual open dyadic validity regions #
The band floor is fixed. A sufficiently small positive physical scale is inside an open validity region of some band above that floor. The local formulas below are supplied on those open regions, rather than by the values of a fixed reference formula on its excluded dyadic faces.
This module transfers local formulas, jets, zero germs, and already proved local endpoint extensions. It does not manufacture their local smoothness or identify them with a reference formula outside its validity region.
A representative on the union of valid open charts #
Local formulas are identified only where both charts are valid. The chosen representative agrees with every valid chart on an ambient neighborhood. No regularity at the boundary of the union is asserted.
Domain, given by ⋃ i, U i.
Equations
- NavierStokes.ValidBandGluing.domain U = ⋃ (i : ι), U i
Instances For
def
NavierStokes.ValidBandGluing.Compatible
{ι : Type u_1}
{D : Type u_2}
{E : Type u_3}
(U : ι → Set D)
(f : ι → D → E)
:
Compatible, given by ∀ i j, EqOn (f i) (f j) (U i ∩ U j).
Equations
- NavierStokes.ValidBandGluing.Compatible U f = ∀ (i j : ι), Set.EqOn (f i) (f j) (U i ∩ U j)
Instances For
noncomputable def
NavierStokes.ValidBandGluing.representative
{ι : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Zero E]
(U : ι → Set D)
(f : ι → D → E)
(x : D)
:
E
Choose a chart only at points covered by at least one valid chart. The value outside the valid union is the stated zero totalization.
Equations
- NavierStokes.ValidBandGluing.representative U f x = if h : ∃ (i : ι), x ∈ U i then f (Classical.choose h) x else 0
Instances For
theorem
NavierStokes.ValidBandGluing.representative_eq_of_mem
{ι : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Zero E]
{U : ι → Set D}
{f : ι → D → E}
(hf : Compatible U f)
{i : ι}
{x : D}
(hx : x ∈ U i)
:
theorem
NavierStokes.ValidBandGluing.representative_eqOn
{ι : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Zero E]
{U : ι → Set D}
{f : ι → D → E}
(hf : Compatible U f)
(i : ι)
:
Set.EqOn (representative U f) (f i) (U i)
theorem
NavierStokes.ValidBandGluing.representative_unique_on_domain
{ι : Type u_1}
{D : Type u_2}
{E : Type u_3}
[Zero E]
{U : ι → Set D}
{f : ι → D → E}
(hf : Compatible U f)
{g : D → E}
(hg : ∀ (i : ι), Set.EqOn g (f i) (U i))
:
Set.EqOn (representative U f) g (domain U)
theorem
NavierStokes.ValidBandGluing.domain_open
{ι : Type u_1}
{D : Type u_2}
[TopologicalSpace D]
{U : ι → Set D}
(hU : ∀ (i : ι), IsOpen (U i))
:
theorem
NavierStokes.ValidBandGluing.representative_germ
{ι : Type u_1}
{D : Type u_2}
{E : Type u_3}
[TopologicalSpace D]
[Zero E]
{U : ι → Set D}
{f : ι → D → E}
(hU : ∀ (i : ι), IsOpen (U i))
(hf : Compatible U f)
{i : ι}
{x : D}
(hx : x ∈ U i)
:
theorem
NavierStokes.ValidBandGluing.representative_zero_germ
{ι : Type u_1}
{D : Type u_2}
{E : Type u_3}
[TopologicalSpace D]
[Zero E]
{U : ι → Set D}
{f : ι → D → E}
{x : D}
(hx : x ∉ closure (domain U))
:
The zero totalization has a zero germ off the closure. No such claim is made at an excluded face in the closure of the valid union.
theorem
NavierStokes.ValidBandGluing.representative_continuousOn
{ι : Type u_1}
{D : Type u_2}
{E : Type u_3}
[TopologicalSpace D]
[TopologicalSpace E]
[Zero E]
{U : ι → Set D}
{f : ι → D → E}
(hU : ∀ (i : ι), IsOpen (U i))
(hf : Compatible U f)
(hs : ∀ (i : ι), ContinuousOn (f i) (U i))
:
ContinuousOn (representative U f) (domain U)
theorem
NavierStokes.ValidBandGluing.representative_contDiffAt
{ι : Type u_1}
{D : Type u_2}
{E : Type u_3}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : ι → Set D}
{f : ι → D → E}
{n : WithTop ℕ∞}
(hU : ∀ (i : ι), IsOpen (U i))
(hf : Compatible U f)
{i : ι}
{x : D}
(hx : x ∈ U i)
(hs : ContDiffOn ℝ n (f i) (U i))
:
ContDiffAt ℝ n (representative U f) x
theorem
NavierStokes.ValidBandGluing.representative_contDiffOn
{ι : Type u_1}
{D : Type u_2}
{E : Type u_3}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : ι → Set D}
{f : ι → D → E}
{n : WithTop ℕ∞}
(hU : ∀ (i : ι), IsOpen (U i))
(hf : Compatible U f)
(hs : ∀ (i : ι), ContDiffOn ℝ n (f i) (U i))
:
ContDiffOn ℝ n (representative U f) (domain U)
theorem
NavierStokes.ValidBandGluing.representative_fderiv_eq
{ι : Type u_1}
{D : Type u_2}
{E : Type u_3}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : ι → Set D}
{f : ι → D → E}
(hU : ∀ (i : ι), IsOpen (U i))
(hf : Compatible U f)
{i : ι}
{x : D}
(hx : x ∈ U i)
:
theorem
NavierStokes.ValidBandGluing.representative_iteratedFDeriv_germ
{ι : Type u_1}
{D : Type u_2}
{E : Type u_3}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : ι → Set D}
{f : ι → D → E}
(hU : ∀ (i : ι), IsOpen (U i))
(hf : Compatible U f)
{i : ι}
{x : D}
(hx : x ∈ U i)
(m : ℕ)
:
The actual multilinear derivative tensors agree as functions near each valid point. No differentiability premise is needed for germ locality.
theorem
NavierStokes.ValidBandGluing.representative_iteratedFDeriv_eq
{ι : Type u_1}
{D : Type u_2}
{E : Type u_3}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : ι → Set D}
{f : ι → D → E}
(hU : ∀ (i : ι), IsOpen (U i))
(hf : Compatible U f)
{i : ι}
{x : D}
(hx : x ∈ U i)
(m : ℕ)
:
theorem
NavierStokes.ValidBandGluing.representative_jet_bound
{ι : Type u_1}
{D : Type u_2}
{E : Type u_3}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : ι → Set D}
{f : ι → D → E}
(hU : ∀ (i : ι), IsOpen (U i))
(hf : Compatible U f)
{i : ι}
{x : D}
(hx : x ∈ U i)
(m : ℕ)
{B : ℝ}
(hb : ‖iteratedFDeriv ℝ m (f i) x‖ ≤ B)
:
theorem
NavierStokes.ValidBandGluing.representative_jet_bound_on_union
{ι : Type u_1}
{D : Type u_2}
{E : Type u_3}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : ι → Set D}
{f : ι → D → E}
(hU : ∀ (i : ι), IsOpen (U i))
(hf : Compatible U f)
(m : ℕ)
{B : D → ℝ}
(hb : ∀ (i : ι), ∀ x ∈ U i, ‖iteratedFDeriv ℝ m (f i) x‖ ≤ B x)
(x : D)
:
x ∈ domain U → ‖iteratedFDeriv ℝ m (representative U f) x‖ ≤ B x
The same pointwise majorant transfers on the entire union. There is no multiplicity factor, regardless of the number of overlapping charts.
theorem
NavierStokes.ValidBandGluing.representative_finite_jets_bound
{ι : Type u_1}
{D : Type u_2}
{E : Type u_3}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : ι → Set D}
{f : ι → D → E}
(hU : ∀ (i : ι), IsOpen (U i))
(hf : Compatible U f)
(N : ℕ)
{B : ℕ → D → ℝ}
(hb : ∀ (i : ι), ∀ m ≤ N, ∀ x ∈ U i, ‖iteratedFDeriv ℝ m (f i) x‖ ≤ B m x)
(m : ℕ)
:
m ≤ N → ∀ x ∈ domain U, ‖iteratedFDeriv ℝ m (representative U f) x‖ ≤ B m x
theorem
NavierStokes.ValidBandGluing.representative_jet_apply_eq
{ι : Type u_1}
{D : Type u_2}
{E : Type u_3}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : ι → Set D}
{f : ι → D → E}
(hU : ∀ (i : ι), IsOpen (U i))
(hf : Compatible U f)
{i : ι}
{x : D}
(hx : x ∈ U i)
(m : ℕ)
(v : Fin m → D)
:
theorem
NavierStokes.ValidBandGluing.spatialCurl_eq_of_germ
{A B : ProblemStatement.VelocityField}
{x : ProblemStatement.SpaceTime}
(h : A =ᶠ[nhds x] B)
:
theorem
NavierStokes.ValidBandGluing.representative_spatialCurl_eq
{ι : Type u_1}
{U : ι → Set ProblemStatement.SpaceTime}
{A : ι → ProblemStatement.VelocityField}
(hU : ∀ (i : ι), IsOpen (U i))
(hA : Compatible U A)
{i : ι}
{x : ProblemStatement.SpaceTime}
(hx : x ∈ U i)
:
theorem
NavierStokes.ValidBandGluing.representative_spatialCurl_germ
{ι : Type u_1}
{U : ι → Set ProblemStatement.SpaceTime}
{A : ι → ProblemStatement.VelocityField}
(hU : ∀ (i : ι), IsOpen (U i))
(hA : Compatible U A)
{i : ι}
{x : ProblemStatement.SpaceTime}
(hx : x ∈ U i)
:
Strictly inside the band: the normalized physical scale is in (1/2,2).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ValidDyadicBandCover.mem_band_iff
{h : ℝ}
{n : ℕ}
{w : ProblemStatement.SpaceTime}
:
w ∈ band h n ↔ w ∈ PhysicalWaveSum.preterminal ∧ PhysicalWaveSum.physicalQ h w / ChartScales.Q n ∈ Set.Ioo (1 / 2) 2
theorem
NavierStokes.ValidDyadicBandCover.exists_band
{h : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(N : ℕ)
{w : ProblemStatement.SpaceTime}
(ht : w ∈ PhysicalWaveSum.preterminal)
(hq : PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q N)
:
∃ (n : ℕ), N ≤ n ∧ w ∈ band h n ∧ PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q n
The selected band has the stronger comparison q ≤ Q_n < 2q.
Charts, given by band h n.val.
Equations
Instances For
theorem
NavierStokes.ValidDyadicBandCover.sublevel_covered
{h qbig : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(N : ℕ)
(hqbig : qbig ≤ ChartScales.Q N)
:
CutStageEstimates.physicalSublevel h qbig ⊆ ValidBandGluing.domain (charts h N)
def
NavierStokes.ValidDyadicBandCover.Compatible
{E : Type u_1}
(h : ℝ)
(N : ℕ)
(f : ℕ → ProblemStatement.SpaceTime → E)
:
Compatible, given by ValidBandGluing.Compatible (charts h N) (fun n => f n.val).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.ValidDyadicBandCover.field
{E : Type u_1}
[NormedAddCommGroup E]
(h : ℝ)
(N : ℕ)
(f : ℕ → ProblemStatement.SpaceTime → E)
:
Field, given by ValidBandGluing.representative (charts h N) (fun n => f n.val).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ValidDyadicBandCover.field_eq
{E : Type u_1}
[NormedAddCommGroup E]
{h : ℝ}
{N n : ℕ}
{f : ℕ → ProblemStatement.SpaceTime → E}
(hf : Compatible h N f)
(hn : N ≤ n)
{w : ProblemStatement.SpaceTime}
(hw : w ∈ band h n)
:
theorem
NavierStokes.ValidDyadicBandCover.field_germ
{E : Type u_1}
[NormedAddCommGroup E]
{h : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
{N n : ℕ}
{f : ℕ → ProblemStatement.SpaceTime → E}
(hf : Compatible h N f)
(hn : N ≤ n)
{w : ProblemStatement.SpaceTime}
(hw : w ∈ band h n)
:
theorem
NavierStokes.ValidDyadicBandCover.field_smooth
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{h qbig : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
{N : ℕ}
{f : ℕ → ProblemStatement.SpaceTime → E}
(hf : Compatible h N f)
(hqbig : qbig ≤ ChartScales.Q N)
(hs : ∀ (n : ℕ), N ≤ n → ContDiffOn ℝ (↑⊤) (f n) (band h n))
:
ContDiffOn ℝ (↑⊤) (field h N f) (CutStageEstimates.physicalSublevel h qbig)
theorem
NavierStokes.ValidDyadicBandCover.field_jet_eq
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{h : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
{N n : ℕ}
{f : ℕ → ProblemStatement.SpaceTime → E}
(hf : Compatible h N f)
(hn : N ≤ n)
{w : ProblemStatement.SpaceTime}
(hw : w ∈ band h n)
(m : ℕ)
:
theorem
NavierStokes.ValidDyadicBandCover.field_jet_bound_at
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{h : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
{N : ℕ}
{f : ℕ → ProblemStatement.SpaceTime → E}
(hf : Compatible h N f)
{w : ProblemStatement.SpaceTime}
(ht : w ∈ PhysicalWaveSum.preterminal)
(hq : PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q N)
(m : ℕ)
{B : ℝ}
(hb :
∀ (n : ℕ), N ≤ n → w ∈ band h n → PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q n → ‖iteratedFDeriv ℝ m (f n) w‖ ≤ B)
:
Pointwise transfer keeps any additional hypotheses on the physical point available to the caller, such as a fixed time bound.
theorem
NavierStokes.ValidDyadicBandCover.field_jet_bound
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{h qbig : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
{N : ℕ}
{f : ℕ → ProblemStatement.SpaceTime → E}
(hf : Compatible h N f)
(hqbig : qbig ≤ ChartScales.Q N)
(m : ℕ)
(B : ProblemStatement.SpaceTime → ℝ)
(hb :
∀ (n : ℕ),
N ≤ n → ∀ w ∈ band h n, PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q n → ‖iteratedFDeriv ℝ m (f n) w‖ ≤ B w)
(w : ProblemStatement.SpaceTime)
:
w ∈ CutStageEstimates.physicalSublevel h qbig → ‖iteratedFDeriv ℝ m (field h N f) w‖ ≤ B w
Select a comparable chart for the bound, independently of the chart
chosen internally by field. No chart-count factor is incurred.
theorem
NavierStokes.ValidDyadicBandCover.field_zero_germ
{E : Type u_1}
[NormedAddCommGroup E]
{h qbig : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
{N : ℕ}
{f : ℕ → ProblemStatement.SpaceTime → E}
(hf : Compatible h N f)
(hqbig : qbig ≤ ChartScales.Q N)
{w : ProblemStatement.SpaceTime}
(hw : w ∈ CutStageEstimates.physicalSublevel h qbig)
(hz : ∀ (n : ℕ), N ≤ n → w ∈ band h n → f n =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0)
:
A local support proof in any valid chart supplies the actual zero germ of the representative, including at the physical axis.
theorem
NavierStokes.ValidDyadicBandCover.endpoint_band
{h : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(N : ℕ)
{x : ProblemStatement.Space}
(hx : x.ofLp 2 ≠ 0)
(hq : EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) ≤ ChartScales.Q N)
:
∃ (n : ℕ),
N ≤ n ∧ ChartScales.Q n / 2 < EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) ∧ EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) < 2 * ChartScales.Q n ∧ ∀ᶠ (w : ProblemStatement.SpaceTime) in nhdsWithin (1, x) (SpacetimeEndpoint.openPast 1), w ∈ band h n
Endpoint selection concerns only the positive limiting scale. The endpoint itself is not inserted into any preterminal formula.
theorem
NavierStokes.ValidDyadicBandCover.field_endpoint_extension
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{h : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
{N : ℕ}
{f : ℕ → ProblemStatement.SpaceTime → E}
(hf : Compatible h N f)
{x : ProblemStatement.Space}
(hx : x.ofLp 2 ≠ 0)
(hq : EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) ≤ ChartScales.Q N)
(he :
∀ (n : ℕ),
N ≤ n →
ChartScales.Q n / 2 < EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) →
EndpointCoordinates.endpointRoot (2 * h) (x.ofLp 2) < 2 * ChartScales.Q n →
Nonempty (JointResidualLimits.OneSidedExtension (f n) x))
:
Nonempty (JointResidualLimits.OneSidedExtension (field h N f) x)
A proved continuation of the selected current-chart formula transfers to the representative. Local continuation remains a necessary premise.