OAI/Combinatorics/HoneycombChords/FourFunctions.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Honeycomb370.rationalGrid line 19
2. theorem OAI.Honeycomb370.continuous_four_functions line 43
3. def OAI.Honeycomb370.orderedBox line 92

   Source documentation

   Closed truncations of the actual ordered positive-node chamber.

   def orderedBox (n : ℕ) (a b : ℝ) : Sublattice (Fin n → ℝ) where
   …

4. lemma OAI.Honeycomb370.orderedBox_closed line 103
5. lemma OAI.Honeycomb370.orderedBox_bounded line 116
6. lemma OAI.Honeycomb370.orderedBox_convex line 122
7. lemma OAI.Honeycomb370.orderedBox_four_functions line 140
8. lemma OAI.Honeycomb370.continuousOn_closed_extension line 166
9. lemma OAI.Honeycomb370.orderedBox_continuousOn_four_functions line 175
10. def OAI.Honeycomb370.orderedPositive line 205
11. lemma OAI.Honeycomb370.orderedPositive_eq_iUnion line 208
12. lemma OAI.Honeycomb370.orderedBox_exhaust_monotone line 228
13. theorem OAI.Honeycomb370.orderedPositive_four_functions line 238

    Source documentation

    Continuous four-functions inequality on the unbounded actual ordered positive-node chamber. Integrability is a pairing-domain obligation, not an association assumption.

    theorem orderedPositive_four_functions (n : ℕ)
        (f₁ f₂ f₃ f₄ : (Fin n → ℝ) → ℝ)
        (hc₁ : ContinuousOn f₁ (orderedPositive n)) (hc₂ : ContinuousOn f₂ (orderedPositive n))
        (hc₃ : ContinuousOn f₃ (orderedPositive n)) (hc₄ : ContinuousOn f₄ (orderedPositive n))
        (hi₁ : IntegrableOn f₁ (orderedPositive n)) (hi₂ : IntegrableOn f₂ (orderedPositive n))
        (hi₃ : IntegrableOn f₃ (orderedPositive n)) (hi₄ : IntegrableOn f₄ (orderedPositive n))
        (h₁ : ∀ x∈orderedPositive n,0≤f₁ x) (h₂ : ∀ x∈orderedPositive n,0≤f₂ x)
        (h₃ : ∀ x∈orderedPositive n,0≤f₃ x) (h₄ : ∀ x∈orderedPositive n,0≤f₄ x)
        (h : ∀ x∈orderedPositive n,∀ y∈orderedPositive n,
          f₁ x*f₂ y≤f₃ (x⊓y)*f₄ (x⊔y)) :
        (∫ x in orderedPositive n,f₁ x)*(∫ x in orderedPositive n,f₂ x) ≤
          (∫ x in orderedPositive n,f₃ x)*(∫ x in orderedPositive n,f₄ x) := by
    …

    Mentions: OAI.Honeycomb370.orderedPositive