OAI/Dynamics/SmoothObstruction/DensityLocalization.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SmoothObstruction.ChartDomination.density_two line 15
2. theorem OAI.SmoothObstruction.ChartDomination.local_two line 28

   Source documentation

   A concrete relative local branch and the two numerical lower bounds give unnormalized domination by TWO in the original carrier measure. No choice of local derivative or branch has to be measurable.

   theorem local_two (μ : Measure X) (m : Measure E) [Measure.IsAddHaarMeasure m]
       (d : E → ℝ) (Q G : Set X) (hQ : μ Qᶜ=0) (hGQ : G⊆Q) (hG : MeasurableSet G)
       (e : X → E) (r : E → X) (he : Measurable e) (hr : Measurable r)
       (hleft : ∀ x∈Q,r (e x)=x) (hcoords : μ.map e=m.withDensity (fun u => ENNReal.ofReal (d u)))
       (f : X → X) (_ : Measurable f) (hfQ : MapsTo f G Q) (hinj : InjOn f G)
       (hlocal : ∀ u∈coordinateSet e r G,∃ g : E → E,
         HasFDerivAt g (fderiv ℝ g u) u ∧ (81/121:ℝ)≤|(fderiv ℝ g u).det| ∧
         g =ᶠ[𝓝[coordinateSet e r G] u] (e ∘ f ∘ r))
       (hd : ∀ u∈coordinateSet e r G,0≤d u ∧ (3/4:ℝ)*d u≤d (e (f (r u)))) :
       (μ.restrict G).map f≤(2 : ℝ≥0∞) • μ := by
   …

   Mentions: OAI.SmoothObstruction.ChartDomination.coordinateSet

3. theorem OAI.SmoothObstruction.ChartDensity.pair_cell_density line 73

   Source documentation

   Product coordinates carry exactly the product of the ORIGINAL cell measures, with its unchanged chart density and no normalization.

   theorem pair_cell_density (hclosed : IsClosed (range I)) (μ : Measure M) [IsFiniteMeasure μ]
       (hμ : SmoothPositiveDensity I μ) (a : M) :
       ∃ f : E₀ → ℝ,ContDiffOn ℝ ∞ f (extChartAt I a).target ∧
         (∀ u∈(extChartAt I a).target,0<f u) ∧
         ∀ Q : Set M,MeasurableSet Q → Q⊆(extChartAt I a).source →
           let W := ChartDomination.coordinateSet (coordinates I a) (inverse I a) Q
   …

   Mentions: OAI.SmoothObstruction.SmoothPositiveDensity, OAI.SmoothObstruction.ChartDomination.coordinateSet, OAI.SmoothObstruction.ChartDensity.coordinates, OAI.SmoothObstruction.ChartDensity.inverse

4. theorem OAI.SmoothObstruction.ChartDensity.pair_cell_two line 121

   Source documentation

   The original-cell change of variables. The density is selected ONCE per atlas chart, before cells or retained pairs. Local branches are only required on the retained relative neighborhood, at every rank including zero.

   theorem pair_cell_two (hclosed : IsClosed (range I)) (μ : Measure M) [IsFiniteMeasure μ]
       (hμ : SmoothPositiveDensity I μ) (a : M) :
       ∃ f : E₀ → ℝ,ContDiffOn ℝ ∞ f (extChartAt I a).target ∧
         (∀ u∈(extChartAt I a).target,0<f u) ∧
         ∀ Q : Set M,MeasurableSet Q → Q⊆(extChartAt I a).source →
         ∀ G : Set (M×M),MeasurableSet G → G⊆Q×ˢQ →
         ∀ Φ : M×M → M×M,Measurable Φ → MapsTo Φ G (Q×ˢQ) → InjOn Φ G →
           let e := Prod.map (coordinates I a) (coordinates I a)
   …

   Mentions: OAI.SmoothObstruction.SmoothPositiveDensity, OAI.SmoothObstruction.ChartDensity.coordinates

5. theorem OAI.SmoothObstruction.DensityUniform.relative line 197

   Source documentation

   Positive compact smooth-chart densities admit uniform relative, rather than absolute, estimates. Only continuity is used, valid up to boundary.

   theorem relative (K : Set E) (hK : IsCompact K) (f : E → ℝ)
       (hf : ContinuousOn f K) (hpos : ∀ x∈K,0<f x) {ε : ℝ} (hε : 0<ε) :
       ∃ δ : ℝ,0<δ ∧ ∀ x∈K,∀ y∈K,dist x y<δ → |f y-f x|≤ε*f x := by
   …

6. theorem OAI.SmoothObstruction.DensityUniform.pair_lower line 215

   Source documentation

   The density portion of the joint switch has a uniform three-quarter lower bound once both matched point pairs are sufficiently close.

   theorem pair_lower (K : Set E) (hK : IsCompact K) (f : E → ℝ)
       (hf : ContinuousOn f K) (hpos : ∀ x∈K,0<f x) :
       ∃ δ : ℝ,0<δ ∧ ∀ x∈K,∀ y∈K,∀ z∈K,∀ w∈K,
         dist x z<δ → dist y w<δ → (3/4:ℝ)*(f x*f y)≤f z*f w := by
   …

7. theorem OAI.SmoothObstruction.ChartDensity.original_law_two line 243

   Source documentation

   The authentic local coordinate germs yield domination of the ORIGINAL cell-weighted experiment. Compact positive density is controlled before any partition or retained set is chosen. Zero-weight cells require no exception, and neither cells nor retained pairs are conditionally renormalized.

   theorem original_law_two (hclosed : IsClosed (range I))
       (μ : Measure M) [IsProbabilityMeasure μ] (hμ : SmoothPositiveDensity I μ)
       (a : ι → M) (K : ι → Set M) (hK : ∀ i,IsCompact (K i))
       (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
       ∃ r : ℝ,0<r ∧ ∀ {J : Type*} [Fintype J] [MeasurableSpace J]
         [MeasurableSingletonClass J] (L : M → J) (c : M → ι) (chart : J → ι),
         Measurable L → (∀ x,x∈K (c x)) → (∀ x,chart (L x)=c x) →
         (∀ x y,L x=L y → ‖coordinates I (a (c x)) x-coordinates I (a (c x)) y‖<r) →
         ∀ (G : Set (M×M)) (Φ : M×M → M×M),MeasurableSet G → Measurable Φ →
         (∀ u∈G,L u.1=L u.2 ∧ L (Φ u).1=L u.1 ∧ L (Φ u).2=L u.2) →
         InjOn Φ G →
         (∀ (j : J),let Q := L ⁻¹' {j}
   …

   Mentions: OAI.SmoothObstruction.SmoothPositiveDensity, OAI.SmoothObstruction.ChartDensity.coordinates

8. theorem OAI.SmoothObstruction.ChartDensity.physical_original_law_two line 336

   Source documentation

   Physical retained-pair germs in their old starting charts suffice for the original cell-weighted, unnormalized domination. The germ is only shrunk when passing to the original cell; no new partition labels are introduced.

   theorem physical_original_law_two (hclosed : IsClosed (range I))
       (μ : Measure M) [IsProbabilityMeasure μ] (hμ : SmoothPositiveDensity I μ)
       (a : ι → M) (K : ι → Set M) (hK : ∀ i,IsCompact (K i))
       (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
       ∃ r : ℝ,0<r ∧ ∀ {J : Type*} [Fintype J] [MeasurableSpace J]
         [MeasurableSingletonClass J] (L : M → J) (c : M → ι) (chart : J → ι),
         Measurable L → (∀ x,x∈K (c x)) → (∀ x,chart (L x)=c x) →
         (∀ x y,L x=L y → ‖coordinates I (a (c x)) x-coordinates I (a (c x)) y‖<r) →
         ∀ (G : Set (M×M)) (Φ : M×M → M×M),MeasurableSet G → Measurable Φ →
         (∀ u∈G,L u.1=L u.2 ∧ L (Φ u).1=L u.1 ∧ L (Φ u).2=L u.2) →
         InjOn Φ G →
         (∀ x y,(x,y)∈G →
   …

   Mentions: OAI.SmoothObstruction.SmoothPositiveDensity, OAI.SmoothObstruction.ChartDensity.coordinates

9. lemma OAI.SmoothObstruction.ManifoldCoordinates.original_coarse_germ line 394

   Source documentation

   The original coarse partition is locally constant at every retained one-point input. This uses the original grid margin and fixed chart core only.

   lemma original_coarse_germ (a : ι → M) (c : M → ι) (P : M → C)
       (x : M) (hx : x∈(chartAt H (a (c x))).source) (s δ : ℝ) (hs : 0<s) (hδ : 0<δ)
       (hcore : ∀ y,dist y x ≤ s → c y=c x)
       (hrec : ∀ y,c y=c x →
         ‖(extChartAt I (a (c x))) y-(extChartAt I (a (c x))) x‖≤δ/4 → P y=P x) :
       ∀ᶠ y in 𝓝 x,P y=P x := by
   …

10. lemma OAI.SmoothObstruction.ManifoldCoordinates.six_original_labels line 412

    Source documentation

    Only the six original start/end labels are fixed near an input pair. No intermediate orbit-code refinement is used.

    lemma six_original_labels (S : Diffeomorph I I M M ∞) (P : M → C)
        (a₀ x y : M) (n : ℕ)
        (hx : x∈(extChartAt I a₀).source) (hy : y∈(extChartAt I a₀).source)
        (hiX : (extChartAt I a₀) x∈interior (range I))
        (hiY : (extChartAt I a₀) y∈interior (range I))
        (hx₀ : ∀ᶠ z in 𝓝 x,P z=P x) (hy₀ : ∀ᶠ z in 𝓝 y,P z=P y)
        (hxF : ∀ᶠ z in 𝓝 (S^[n] x),P z=P (S^[n] x))
        (hyF : ∀ᶠ z in 𝓝 (S^[n] y),P z=P (S^[n] y))
        (hxB : ∀ᶠ z in 𝓝 (S.symm^[n] x),P z=P (S.symm^[n] x))
        (hyB : ∀ᶠ z in 𝓝 (S.symm^[n] y),P z=P (S.symm^[n] y)) :
        ∀ᶠ t in 𝓝 ((extChartAt I a₀ x),(extChartAt I a₀ y)),
          P ((extChartAt I a₀).symm t.1)=P x ∧ P ((extChartAt I a₀).symm t.2)=P y ∧
    …

11. theorem OAI.SmoothObstruction.ManifoldCoordinates.genuine_pair_switch line 460

    Source documentation

    The genuine global pair switch at one scale. Every constant precedes the partition alphabets and ranks. Inputs are actual bilateral gauges, original grid margins, and explicit scalar budgets; the conclusion is unnormalized ORIGINAL-law domination, not an assumed Jacobian or switch certificate.

    theorem genuine_pair_switch (hclosed : IsClosed (range I))
        (μ : Measure M) [IsProbabilityMeasure μ] (hμ : SmoothPositiveDensity I μ)
        (S : Diffeomorph I I M M ∞) (a : ι → M) (K : ι → Set M)
        (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source)
        (s Dg : ℝ) (hs : 0<s) (hDg : 0≤Dg) :
        ∃ r₀ C₀ σ r₁ C₁ rg Cg β K₀F CreF C₁F K₀B CreB C₁B rμ : ℝ,
          0<r₀ ∧ 1≤C₀ ∧ 0<σ ∧ 0<r₁ ∧ 1≤C₁ ∧ 0<rg ∧ 1≤Cg ∧ 0<β ∧
          1≤K₀F ∧ 0≤CreF ∧ 0≤C₁F ∧ 1≤K₀B ∧ 0≤CreB ∧ 0≤C₁B ∧ 0<rμ ∧
          ∀ {C J : Type*} [Fintype C] [MeasurableSpace C] [MeasurableSingletonClass C]
            [Fintype J] [MeasurableSpace J] [MeasurableSingletonClass J]
            (c : M → ι) (P : M → C) (L : M → J) (π : J → C) (chart : C → ι)
            (G R V Wc Wp : Set M) (n : ℕ) (b R₀ Cext ε g α r δc δp H₀ : ℝ)
    …

    Mentions: OAI.SmoothObstruction.SmoothPositiveDensity