OAI/Analysis/MassAction/AffineFamilyGluing.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem326.Affine.Label.shiftOffset line 17

   Source documentation

   Shift an affine label without changing its slope.

   def Label.shiftOffset {d : ℕ} (L : Label d) (s : ℝ → ℝ) : Label d :=
   …

   Mentions: OAI.Problem326.Affine.Label

2. theorem OAI.Problem326.Affine.Label.shiftOffset_slope line 20
3. theorem OAI.Problem326.Affine.Label.shiftOffset_value line 23
4. def OAI.Problem326.Affine.shiftedFamily line 30

   Source documentation

   The finite union of shifted local families; duplicate labels are harmless.

   def shiftedFamily {d : ℕ} {ι : Type uIota} [Fintype ι]
       (Λ : ι → Finset (Label d)) (s : ι → ℝ → ℝ) : Finset (Label d) := by
   …

   Mentions: OAI.Problem326.Affine.Label

5. theorem OAI.Problem326.Affine.mem_shiftedFamily_iff line 35
6. theorem OAI.Problem326.Affine.shiftOffset_mem_shiftedFamily line 41
7. theorem OAI.Problem326.Affine.active_shiftedFamily_restrict line 47
8. def OAI.Problem326.Affine.extendedCut line 59

   Source documentation

   An arbitrary total extension is only used at valid cut indices.

   def extendedCut {n : ℕ} (q : Fin n → ℝ) (k : ℕ) : ℝ :=
   …

9. theorem OAI.Problem326.Affine.extendedCut_fin line 62
10. def OAI.Problem326.Affine.cutShift line 66

    Source documentation

    Cumulative shifts select a local family on the corresponding exponent cell.

    def cutShift {n : ℕ} (q : Fin n → ℝ) (j : Fin (n + 1)) (h : ℝ) : ℝ :=
    …

11. def OAI.Problem326.Affine.InCutCell line 70

    Source documentation

    Closed cells include tied transition points.

    def InCutCell {n : ℕ} (q : Fin n → ℝ) (a b : ℝ)
        (j : Fin (n + 1)) (μ : ℝ) : Prop :=
    …

12. theorem OAI.Problem326.Affine.active_shiftedFamily_upper_cut line 78

    Source documentation

    Actual canonical label activity supplies the upper-cut inequality needed by the asymptotic neighboring-family comparison.

    theorem active_shiftedFamily_upper_cut {d n : ℕ}
        (Λ : Fin (n + 1) → Finset (Label d))
        (q : Fin n → ℝ) (t : Fin (n + 1) → ℝ)
        (hbase : ∀ j, (⟨fun _ => t j, fun _ => 0⟩ : Label d) ∈ Λ j)
        (i : Fin n) {L : Label d}
        (h : ℕ → ℝ) (p : ℕ → (Fin d → ℝ)) (p₀ : Fin d → ℝ)
        (hpos : ∀ k, 0 < h k) (hh : Tendsto h atTop (𝓝 0))
        (hp : Tendsto p atTop (𝓝 p₀))
        (hoff : L.offset =o[𝓝[>] (0 : ℝ)] (fun h => h ^ q i))
        (hA : ∀ k, Active (shiftedFamily Λ (cutShift q))
          (L.shiftOffset (cutShift q i.castSucc)) (h k) (powerPoint (h k) (p k))) :
        ∃ k, p₀ k ≤ q i := by
    …

    Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.Active, OAI.Problem326.Affine.shiftedFamily, OAI.Problem326.Affine.cutShift, OAI.Problem326.Affine.powerPoint

13. theorem OAI.Problem326.Affine.active_shiftedFamily_lower_cut line 111

    Source documentation

    The corresponding lower-cut conclusion, using the strict slope gap to the preceding baseline.

    theorem active_shiftedFamily_lower_cut {d n : ℕ}
        (Λ : Fin (n + 1) → Finset (Label d))
        (q : Fin n → ℝ) (t : Fin (n + 1) → ℝ)
        (hbase : ∀ j, (⟨fun _ => t j, fun _ => 0⟩ : Label d) ∈ Λ j)
        (i : Fin n) {L : Label d} (hr : ∀ k, t i.castSucc < L.slope k)
        (h : ℕ → ℝ) (p : ℕ → (Fin d → ℝ)) (p₀ : Fin d → ℝ)
        (hpos : ∀ k, 0 < h k) (hh : Tendsto h atTop (𝓝 0))
        (hp : Tendsto p atTop (𝓝 p₀))
        (hoff : L.offset =o[𝓝[>] (0 : ℝ)] (fun h => h ^ q i))
        (hA : ∀ k, Active (shiftedFamily Λ (cutShift q))
          (L.shiftOffset (cutShift q i.succ)) (h k) (powerPoint (h k) (p k))) :
        ∀ k, q i ≤ p₀ k := by
    …

    Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.Active, OAI.Problem326.Affine.shiftedFamily, OAI.Problem326.Affine.cutShift, OAI.Problem326.Affine.powerPoint

14. theorem OAI.Problem326.Affine.approximatesOnCube_shiftedFamily_of_cells line 147

    Source documentation

    Assemble the global sequential approximation statement from local cell statements. All activity is activity of the actual finite union of shifted canonical labels; no analytically unsupported preferred minimizer is selected.

    theorem approximatesOnCube_shiftedFamily_of_cells {d n : ℕ} [NeZero d]
        (Λ : Fin (n + 1) → Finset (Label d))
        (q : Fin n → ℝ) (t : Fin (n + 1) → ℝ)
        (a b : ℝ) (E : (Fin d → ℝ) → ℝ)
        (ht : StrictMono t)
        (hbase : ∀ j, (⟨fun _ => t j, fun _ => 0⟩ : Label d) ∈ Λ j)
        (hslope : ∀ j, ∀ L ∈ Λ j, ∀ k, t j ≤ L.slope k)
        (hoffUpper : ∀ i : Fin n, ∀ L ∈ Λ i.castSucc,
          L.offset =o[𝓝[>] (0 : ℝ)] (fun h => h ^ q i))
        (hoffLower : ∀ i : Fin n, ∀ L ∈ Λ i.succ,
          L.offset =o[𝓝[>] (0 : ℝ)] (fun h => h ^ q i))
        (hlocal : ∀ j, ∀ L ∈ Λ j,
    …

    Mentions: OAI.Problem326.Affine.Label

15. theorem OAI.Problem326.Affine.cutShift_isLittleO line 194

    Source documentation

    Every cumulative cut shift is negligible at the original lower exponent.

    theorem cutShift_isLittleO {n : ℕ} (q : Fin n → ℝ) (a : ℝ)
        (hq : ∀ i, a < q i) (j : Fin (n + 1)) :
        cutShift q j =o[𝓝[>] (0 : ℝ)] (fun h => h ^ a) := by
    …

    Mentions: OAI.Problem326.Affine.cutShift

16. theorem OAI.Problem326.Affine.shiftedFamily_properties line 211

    Source documentation

    The union stays nonempty, preserves slope bounds, and preserves the required offset decay after all cumulative shifts.

    theorem shiftedFamily_properties {d n : ℕ}
        (Λ : Fin (n + 1) → Finset (Label d)) (q : Fin n → ℝ) (a b : ℝ)
        (hne : (Λ 0).Nonempty)
        (hslopes : ∀ j, ∀ L ∈ Λ j, Cube a b L.slope)
        (hoff : ∀ j, ∀ L ∈ Λ j, L.offset =o[𝓝[>] (0 : ℝ)] (fun h => h ^ a))
        (hq : ∀ i, a < q i) :
        (shiftedFamily Λ (cutShift q)).Nonempty ∧
          ∀ J ∈ shiftedFamily Λ (cutShift q), Cube a b J.slope ∧
            J.offset =o[𝓝[>] (0 : ℝ)] (fun h => h ^ a) := by
    …

    Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.Cube, OAI.Problem326.Affine.shiftedFamily, OAI.Problem326.Affine.cutShift